Termination proof of /tmp/tmphnCSrz/AlternatingGrowReduceRec2.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 420 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1120 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 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 (⇒, 140 ms)

        ↳20 IDP

        ↳21 IDPNonInfProof (⇒, 150 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:
807_0_growReduce_NONNULL(EOS(STATIC_807), i84, java.lang.Object(o132sub), java.lang.Object(o132sub)) → 809_0_growReduce_NONNULL(EOS(STATIC_809), i84, java.lang.Object(o132sub), java.lang.Object(o132sub))
809_0_growReduce_NONNULL(EOS(STATIC_809), i84, java.lang.Object(o132sub), java.lang.Object(o132sub)) → 812_0_growReduce_Load(EOS(STATIC_812), i84, java.lang.Object(o132sub))
812_0_growReduce_Load(EOS(STATIC_812), i84, java.lang.Object(o132sub)) → 816_0_growReduce_NE(EOS(STATIC_816), i84, java.lang.Object(o132sub), i84)
816_0_growReduce_NE(EOS(STATIC_816), i87, java.lang.Object(o132sub), i87) → 820_0_growReduce_NE(EOS(STATIC_820), i87, java.lang.Object(o132sub), i87)
816_0_growReduce_NE(EOS(STATIC_816), matching1, java.lang.Object(o132sub), matching2) → 821_0_growReduce_NE(EOS(STATIC_821), 0, java.lang.Object(o132sub), 0) | &&(=(matching1, 0), =(matching2, 0))
820_0_growReduce_NE(EOS(STATIC_820), i87, java.lang.Object(o132sub), i87) → 824_0_growReduce_Load(EOS(STATIC_824), i87, java.lang.Object(o132sub)) | >(i87, 0)
824_0_growReduce_Load(EOS(STATIC_824), i87, java.lang.Object(o132sub)) → 829_0_growReduce_ConstantStackPush(EOS(STATIC_829), i87, java.lang.Object(o132sub), i87)
829_0_growReduce_ConstantStackPush(EOS(STATIC_829), i87, java.lang.Object(o132sub), i87) → 836_0_growReduce_NE(EOS(STATIC_836), i87, java.lang.Object(o132sub), i87, 1)
836_0_growReduce_NE(EOS(STATIC_836), matching1, java.lang.Object(o132sub), matching2, matching3) → 840_0_growReduce_NE(EOS(STATIC_840), 1, java.lang.Object(o132sub), 1, 1) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
836_0_growReduce_NE(EOS(STATIC_836), matching1, java.lang.Object(o132sub), matching2, matching3) → 841_0_growReduce_NE(EOS(STATIC_841), 2, java.lang.Object(o132sub), 2, 1) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
840_0_growReduce_NE(EOS(STATIC_840), matching1, java.lang.Object(o132sub), matching2, matching3) → 847_0_growReduce_New(EOS(STATIC_847), 1, java.lang.Object(o132sub)) | &&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1))
847_0_growReduce_New(EOS(STATIC_847), matching1, java.lang.Object(o132sub)) → 856_0_growReduce_Duplicate(EOS(STATIC_856), 1, java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
856_0_growReduce_Duplicate(EOS(STATIC_856), matching1, java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 862_0_growReduce_Load(EOS(STATIC_862), 1, java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
862_0_growReduce_Load(EOS(STATIC_862), matching1, java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 871_0_growReduce_InvokeMethod(EOS(STATIC_871), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) | =(matching1, 1)
871_0_growReduce_InvokeMethod(EOS(STATIC_871), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) → 879_0_<init>_Load(EOS(STATIC_879), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) | =(matching1, 1)
879_0_<init>_Load(EOS(STATIC_879), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) → 900_0_<init>_InvokeMethod(EOS(STATIC_900), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
900_0_<init>_InvokeMethod(EOS(STATIC_900), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 911_0_<init>_Load(EOS(STATIC_911), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) | =(matching1, 1)
911_0_<init>_Load(EOS(STATIC_911), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) → 924_0_<init>_Load(EOS(STATIC_924), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 1)
924_0_<init>_Load(EOS(STATIC_924), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 936_0_<init>_FieldAccess(EOS(STATIC_936), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) | =(matching1, 1)
936_0_<init>_FieldAccess(EOS(STATIC_936), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o132sub)) → 949_0_<init>_Return(EOS(STATIC_949), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), java.lang.Object(o132sub)) | =(matching1, 1)
949_0_<init>_Return(EOS(STATIC_949), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), java.lang.Object(o132sub)) → 960_0_growReduce_Store(EOS(STATIC_960), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 1)
960_0_growReduce_Store(EOS(STATIC_960), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 966_0_growReduce_JMP(EOS(STATIC_966), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 1)
966_0_growReduce_JMP(EOS(STATIC_966), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 982_0_growReduce_Inc(EOS(STATIC_982), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 1)
982_0_growReduce_Inc(EOS(STATIC_982), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 996_0_growReduce_Load(EOS(STATIC_996), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 1)
996_0_growReduce_Load(EOS(STATIC_996), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 1004_0_growReduce_ConstantStackPush(EOS(STATIC_1004), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), 2) | =(matching1, 2)
1004_0_growReduce_ConstantStackPush(EOS(STATIC_1004), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), matching2) → 1014_0_growReduce_LE(EOS(STATIC_1014), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), 2, 2) | &&(=(matching1, 2), =(matching2, 2))
1014_0_growReduce_LE(EOS(STATIC_1014), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), matching2, matching3) → 1026_0_growReduce_Load(EOS(STATIC_1026), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 2))
1026_0_growReduce_Load(EOS(STATIC_1026), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 1042_0_growReduce_Load(EOS(STATIC_1042), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), 2) | =(matching1, 2)
1042_0_growReduce_Load(EOS(STATIC_1042), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub))), matching1) → 1071_0_growReduce_InvokeMethod(EOS(STATIC_1071), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 2)
1071_0_growReduce_InvokeMethod(EOS(STATIC_1071), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 1100_1_growReduce_InvokeMethod(1100_0_growReduce_Load(EOS(STATIC_1100), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 2)
1100_0_growReduce_Load(EOS(STATIC_1100), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 1112_0_growReduce_Load(EOS(STATIC_1112), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 2)
1112_0_growReduce_Load(EOS(STATIC_1112), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) → 1137_0_growReduce_Load(EOS(STATIC_1137), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o132sub)))) | =(matching1, 2)
1137_0_growReduce_Load(EOS(STATIC_1137), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o129))) → 800_0_growReduce_Load(EOS(STATIC_800), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o129))) | =(matching1, 2)
800_0_growReduce_Load(EOS(STATIC_800), i84, o128) → 807_0_growReduce_NONNULL(EOS(STATIC_807), i84, o128, o128)
841_0_growReduce_NE(EOS(STATIC_841), matching1, java.lang.Object(o132sub), matching2, matching3) → 849_0_growReduce_Load(EOS(STATIC_849), 2, java.lang.Object(o132sub)) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
849_0_growReduce_Load(EOS(STATIC_849), matching1, java.lang.Object(o132sub)) → 858_0_growReduce_ConstantStackPush(EOS(STATIC_858), 2, java.lang.Object(o132sub), 2) | =(matching1, 2)
858_0_growReduce_ConstantStackPush(EOS(STATIC_858), matching1, java.lang.Object(o132sub), matching2) → 864_0_growReduce_LE(EOS(STATIC_864), 2, java.lang.Object(o132sub), 2, 1) | &&(=(matching1, 2), =(matching2, 2))
864_0_growReduce_LE(EOS(STATIC_864), matching1, java.lang.Object(o132sub), matching2, matching3) → 873_0_growReduce_Load(EOS(STATIC_873), 2, java.lang.Object(o132sub)) | &&(&&(=(matching1, 2), =(matching2, 2)), =(matching3, 1))
873_0_growReduce_Load(EOS(STATIC_873), matching1, java.lang.Object(o132sub)) → 883_0_growReduce_FieldAccess(EOS(STATIC_883), 2, java.lang.Object(o132sub)) | =(matching1, 2)
883_0_growReduce_FieldAccess(EOS(STATIC_883), matching1, java.lang.Object(o132sub)) → 892_0_growReduce_FieldAccess(EOS(STATIC_892), 2, java.lang.Object(o132sub)) | =(matching1, 2)
883_0_growReduce_FieldAccess(EOS(STATIC_883), matching1, java.lang.Object(o132sub)) → 893_0_growReduce_FieldAccess(EOS(STATIC_893), 2, java.lang.Object(o132sub)) | =(matching1, 2)
892_0_growReduce_FieldAccess(EOS(STATIC_892), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o164))) → 903_0_growReduce_FieldAccess(EOS(STATIC_903), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o164))) | =(matching1, 2)
903_0_growReduce_FieldAccess(EOS(STATIC_903), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o164))) → 914_0_growReduce_Store(EOS(STATIC_914), 2, o164) | =(matching1, 2)
914_0_growReduce_Store(EOS(STATIC_914), matching1, o164) → 927_0_growReduce_Inc(EOS(STATIC_927), 2, o164) | =(matching1, 2)
927_0_growReduce_Inc(EOS(STATIC_927), matching1, o164) → 939_0_growReduce_Load(EOS(STATIC_939), o164) | =(matching1, 2)
939_0_growReduce_Load(EOS(STATIC_939), o164) → 952_0_growReduce_ConstantStackPush(EOS(STATIC_952), o164)
952_0_growReduce_ConstantStackPush(EOS(STATIC_952), o164) → 962_0_growReduce_LE(EOS(STATIC_962), o164, 2)
962_0_growReduce_LE(EOS(STATIC_962), o164, matching1) → 968_0_growReduce_ConstantStackPush(EOS(STATIC_968), o164) | =(matching1, 2)
968_0_growReduce_ConstantStackPush(EOS(STATIC_968), o164) → 984_0_growReduce_Load(EOS(STATIC_984), o164, 0)
984_0_growReduce_Load(EOS(STATIC_984), o164, matching1) → 997_0_growReduce_InvokeMethod(EOS(STATIC_997), 0, o164) | =(matching1, 0)
997_0_growReduce_InvokeMethod(EOS(STATIC_997), matching1, o164) → 1005_1_growReduce_InvokeMethod(1005_0_growReduce_Load(EOS(STATIC_1005), 0, o164), 0, o164) | =(matching1, 0)
1005_0_growReduce_Load(EOS(STATIC_1005), matching1, o164) → 1016_0_growReduce_Load(EOS(STATIC_1016), 0, o164) | =(matching1, 0)
1016_0_growReduce_Load(EOS(STATIC_1016), matching1, o164) → 800_0_growReduce_Load(EOS(STATIC_800), 0, o164) | =(matching1, 0)
893_0_growReduce_FieldAccess(EOS(STATIC_893), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o166))) → 905_0_growReduce_FieldAccess(EOS(STATIC_905), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o166))) | =(matching1, 2)
905_0_growReduce_FieldAccess(EOS(STATIC_905), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o166))) → 917_0_growReduce_Store(EOS(STATIC_917), 2, o166) | =(matching1, 2)
917_0_growReduce_Store(EOS(STATIC_917), matching1, o166) → 930_0_growReduce_Inc(EOS(STATIC_930), 2, o166) | =(matching1, 2)
930_0_growReduce_Inc(EOS(STATIC_930), matching1, o166) → 942_0_growReduce_Load(EOS(STATIC_942), o166) | =(matching1, 2)
942_0_growReduce_Load(EOS(STATIC_942), o166) → 955_0_growReduce_ConstantStackPush(EOS(STATIC_955), o166)
955_0_growReduce_ConstantStackPush(EOS(STATIC_955), o166) → 964_0_growReduce_LE(EOS(STATIC_964), o166, 2)
964_0_growReduce_LE(EOS(STATIC_964), o166, matching1) → 970_0_growReduce_ConstantStackPush(EOS(STATIC_970), o166) | =(matching1, 2)
970_0_growReduce_ConstantStackPush(EOS(STATIC_970), o166) → 986_0_growReduce_Load(EOS(STATIC_986), o166, 0)
986_0_growReduce_Load(EOS(STATIC_986), o166, matching1) → 1000_0_growReduce_InvokeMethod(EOS(STATIC_1000), 0, o166) | =(matching1, 0)
1000_0_growReduce_InvokeMethod(EOS(STATIC_1000), matching1, o166) → 1008_1_growReduce_InvokeMethod(1008_0_growReduce_Load(EOS(STATIC_1008), 0, o166), 0, o166) | =(matching1, 0)
1008_0_growReduce_Load(EOS(STATIC_1008), matching1, o166) → 1017_0_growReduce_Load(EOS(STATIC_1017), 0, o166) | =(matching1, 0)
1017_0_growReduce_Load(EOS(STATIC_1017), matching1, o166) → 1066_0_growReduce_Load(EOS(STATIC_1066), 0, o166) | =(matching1, 0)
1066_0_growReduce_Load(EOS(STATIC_1066), matching1, o166) → 800_0_growReduce_Load(EOS(STATIC_800), 0, o166) | =(matching1, 0)
821_0_growReduce_NE(EOS(STATIC_821), matching1, java.lang.Object(o132sub), matching2) → 826_0_growReduce_Load(EOS(STATIC_826), 0, java.lang.Object(o132sub)) | &&(=(matching1, 0), =(matching2, 0))
826_0_growReduce_Load(EOS(STATIC_826), matching1, java.lang.Object(o132sub)) → 833_0_growReduce_FieldAccess(EOS(STATIC_833), 0, java.lang.Object(o132sub)) | =(matching1, 0)
833_0_growReduce_FieldAccess(EOS(STATIC_833), matching1, java.lang.Object(o132sub)) → 838_0_growReduce_FieldAccess(EOS(STATIC_838), 0, java.lang.Object(o132sub)) | =(matching1, 0)
833_0_growReduce_FieldAccess(EOS(STATIC_833), matching1, java.lang.Object(o132sub)) → 839_0_growReduce_FieldAccess(EOS(STATIC_839), 0, java.lang.Object(o132sub)) | =(matching1, 0)
838_0_growReduce_FieldAccess(EOS(STATIC_838), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) → 843_0_growReduce_FieldAccess(EOS(STATIC_843), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) | =(matching1, 0)
843_0_growReduce_FieldAccess(EOS(STATIC_843), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o134))) → 851_0_growReduce_Store(EOS(STATIC_851), 0, o134) | =(matching1, 0)
851_0_growReduce_Store(EOS(STATIC_851), matching1, o134) → 860_0_growReduce_JMP(EOS(STATIC_860), 0, o134) | =(matching1, 0)
860_0_growReduce_JMP(EOS(STATIC_860), matching1, o134) → 866_0_growReduce_Inc(EOS(STATIC_866), 0, o134) | =(matching1, 0)
866_0_growReduce_Inc(EOS(STATIC_866), matching1, o134) → 875_0_growReduce_Load(EOS(STATIC_875), 1, o134) | =(matching1, 0)
875_0_growReduce_Load(EOS(STATIC_875), matching1, o134) → 885_0_growReduce_ConstantStackPush(EOS(STATIC_885), 1, o134, 1) | =(matching1, 1)
885_0_growReduce_ConstantStackPush(EOS(STATIC_885), matching1, o134, matching2) → 895_0_growReduce_LE(EOS(STATIC_895), 1, o134, 1) | &&(=(matching1, 1), =(matching2, 1))
895_0_growReduce_LE(EOS(STATIC_895), matching1, o134, matching2) → 906_0_growReduce_Load(EOS(STATIC_906), 1, o134) | &&(=(matching1, 1), =(matching2, 1))
906_0_growReduce_Load(EOS(STATIC_906), matching1, o134) → 919_0_growReduce_Load(EOS(STATIC_919), o134, 1) | =(matching1, 1)
919_0_growReduce_Load(EOS(STATIC_919), o134, matching1) → 932_0_growReduce_InvokeMethod(EOS(STATIC_932), 1, o134) | =(matching1, 1)
932_0_growReduce_InvokeMethod(EOS(STATIC_932), matching1, o134) → 944_1_growReduce_InvokeMethod(944_0_growReduce_Load(EOS(STATIC_944), 1, o134), 1, o134) | =(matching1, 1)
944_0_growReduce_Load(EOS(STATIC_944), matching1, o134) → 957_0_growReduce_Load(EOS(STATIC_957), 1, o134) | =(matching1, 1)
957_0_growReduce_Load(EOS(STATIC_957), matching1, o134) → 800_0_growReduce_Load(EOS(STATIC_800), 1, o134) | =(matching1, 1)
839_0_growReduce_FieldAccess(EOS(STATIC_839), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) → 845_0_growReduce_FieldAccess(EOS(STATIC_845), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) | =(matching1, 0)
845_0_growReduce_FieldAccess(EOS(STATIC_845), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o136))) → 854_0_growReduce_Store(EOS(STATIC_854), 0, o136) | =(matching1, 0)
854_0_growReduce_Store(EOS(STATIC_854), matching1, o136) → 861_0_growReduce_JMP(EOS(STATIC_861), 0, o136) | =(matching1, 0)
861_0_growReduce_JMP(EOS(STATIC_861), matching1, o136) → 869_0_growReduce_Inc(EOS(STATIC_869), 0, o136) | =(matching1, 0)
869_0_growReduce_Inc(EOS(STATIC_869), matching1, o136) → 877_0_growReduce_Load(EOS(STATIC_877), 1, o136) | =(matching1, 0)
877_0_growReduce_Load(EOS(STATIC_877), matching1, o136) → 888_0_growReduce_ConstantStackPush(EOS(STATIC_888), 1, o136, 1) | =(matching1, 1)
888_0_growReduce_ConstantStackPush(EOS(STATIC_888), matching1, o136, matching2) → 898_0_growReduce_LE(EOS(STATIC_898), 1, o136, 1) | &&(=(matching1, 1), =(matching2, 1))
898_0_growReduce_LE(EOS(STATIC_898), matching1, o136, matching2) → 908_0_growReduce_Load(EOS(STATIC_908), 1, o136) | &&(=(matching1, 1), =(matching2, 1))
908_0_growReduce_Load(EOS(STATIC_908), matching1, o136) → 922_0_growReduce_Load(EOS(STATIC_922), o136, 1) | =(matching1, 1)
922_0_growReduce_Load(EOS(STATIC_922), o136, matching1) → 934_0_growReduce_InvokeMethod(EOS(STATIC_934), 1, o136) | =(matching1, 1)
934_0_growReduce_InvokeMethod(EOS(STATIC_934), matching1, o136) → 945_1_growReduce_InvokeMethod(945_0_growReduce_Load(EOS(STATIC_945), 1, o136), 1, o136) | =(matching1, 1)
945_0_growReduce_Load(EOS(STATIC_945), matching1, o136) → 958_0_growReduce_Load(EOS(STATIC_958), 1, o136) | =(matching1, 1)
958_0_growReduce_Load(EOS(STATIC_958), matching1, o136) → 980_0_growReduce_Load(EOS(STATIC_980), 1, o136) | =(matching1, 1)
980_0_growReduce_Load(EOS(STATIC_980), matching1, o136) → 800_0_growReduce_Load(EOS(STATIC_800), 1, o136) | =(matching1, 1)
R rules:
807_0_growReduce_NONNULL(EOS(STATIC_807), i84, NULL, NULL) → 810_0_growReduce_NONNULL(EOS(STATIC_810), i84, NULL, NULL)
810_0_growReduce_NONNULL(EOS(STATIC_810), i84, NULL, NULL) → 814_0_growReduce_Return(EOS(STATIC_814), i84, NULL)
944_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), matching1, NULL), matching2, NULL) → 987_0_growReduce_Return(EOS(STATIC_987), 1, NULL, 1, NULL) | &&(=(matching1, 1), =(matching2, 1))
944_1_growReduce_InvokeMethod(1383_0_growReduce_Return(EOS(STATIC_1383)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o579))) → 1402_0_growReduce_Return(EOS(STATIC_1402), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o579))) | =(matching1, 1)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), matching1, NULL), matching2, NULL) → 1003_0_growReduce_Return(EOS(STATIC_1003), 1, NULL, 1, NULL) | &&(=(matching1, 1), =(matching2, 1))
945_1_growReduce_InvokeMethod(1383_0_growReduce_Return(EOS(STATIC_1383)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o583))) → 1410_0_growReduce_Return(EOS(STATIC_1410), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o583))) | =(matching1, 1)
987_0_growReduce_Return(EOS(STATIC_987), matching1, NULL, matching2, NULL) → 1001_0_growReduce_Return(EOS(STATIC_1001)) | &&(=(matching1, 1), =(matching2, 1))
1001_0_growReduce_Return(EOS(STATIC_1001)) → 1012_0_growReduce_Return(EOS(STATIC_1012))
1003_0_growReduce_Return(EOS(STATIC_1003), matching1, NULL, matching2, NULL) → 1012_0_growReduce_Return(EOS(STATIC_1012)) | &&(=(matching1, 1), =(matching2, 1))
1005_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), matching1, NULL), matching2, NULL) → 1072_0_growReduce_Return(EOS(STATIC_1072), 0, NULL, 0, NULL) | &&(=(matching1, 0), =(matching2, 0))
1005_1_growReduce_InvokeMethod(1001_0_growReduce_Return(EOS(STATIC_1001)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1073_0_growReduce_Return(EOS(STATIC_1073), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1005_1_growReduce_InvokeMethod(1012_0_growReduce_Return(EOS(STATIC_1012)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1081_0_growReduce_Return(EOS(STATIC_1081), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1005_1_growReduce_InvokeMethod(1418_0_growReduce_Return(EOS(STATIC_1418)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) → 1456_0_growReduce_Return(EOS(STATIC_1456), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) | =(matching1, 0)
1005_1_growReduce_InvokeMethod(1422_0_growReduce_Return(EOS(STATIC_1422)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) → 1468_0_growReduce_Return(EOS(STATIC_1468), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) | =(matching1, 0)
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), matching1, NULL), matching2, NULL) → 1105_0_growReduce_Return(EOS(STATIC_1105), 0, NULL, 0, NULL) | &&(=(matching1, 0), =(matching2, 0))
1008_1_growReduce_InvokeMethod(1001_0_growReduce_Return(EOS(STATIC_1001)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1106_0_growReduce_Return(EOS(STATIC_1106), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return(EOS(STATIC_1012)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1109_0_growReduce_Return(EOS(STATIC_1109), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1008_1_growReduce_InvokeMethod(1418_0_growReduce_Return(EOS(STATIC_1418)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) → 1459_0_growReduce_Return(EOS(STATIC_1459), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) | =(matching1, 0)
1008_1_growReduce_InvokeMethod(1422_0_growReduce_Return(EOS(STATIC_1422)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o679))))) → 1470_0_growReduce_Return(EOS(STATIC_1470), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o679))))) | =(matching1, 0)
1072_0_growReduce_Return(EOS(STATIC_1072), matching1, NULL, matching2, NULL) → 1101_0_growReduce_JMP(EOS(STATIC_1101)) | &&(=(matching1, 0), =(matching2, 0))
1073_0_growReduce_Return(EOS(STATIC_1073), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1082_0_growReduce_Return(EOS(STATIC_1082), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1081_0_growReduce_Return(EOS(STATIC_1081), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1082_0_growReduce_Return(EOS(STATIC_1082), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1082_0_growReduce_Return(EOS(STATIC_1082), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1294_0_growReduce_Return(EOS(STATIC_1294), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1100_1_growReduce_InvokeMethod(1330_0_growReduce_Return(EOS(STATIC_1330)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o545))))) → 1371_0_growReduce_Return(EOS(STATIC_1371), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o545))))) | =(matching1, 2)
1100_1_growReduce_InvokeMethod(1335_0_growReduce_Return(EOS(STATIC_1335)), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o550))))) → 1381_0_growReduce_Return(EOS(STATIC_1381), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o550))))) | =(matching1, 2)
1101_0_growReduce_JMP(EOS(STATIC_1101)) → 1121_0_growReduce_JMP(EOS(STATIC_1121))
1105_0_growReduce_Return(EOS(STATIC_1105), matching1, NULL, matching2, NULL) → 1121_0_growReduce_JMP(EOS(STATIC_1121)) | &&(=(matching1, 0), =(matching2, 0))
1106_0_growReduce_Return(EOS(STATIC_1106), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1305_0_growReduce_Return(EOS(STATIC_1305), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1109_0_growReduce_Return(EOS(STATIC_1109), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1106_0_growReduce_Return(EOS(STATIC_1106), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
1121_0_growReduce_JMP(EOS(STATIC_1121)) → 1129_0_growReduce_Return(EOS(STATIC_1129))
1193_0_growReduce_Return(EOS(STATIC_1193), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))))) → 1372_0_growReduce_Return(EOS(STATIC_1372), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))))) | =(matching1, 2)
1294_0_growReduce_Return(EOS(STATIC_1294), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o438))) → 1323_0_growReduce_JMP(EOS(STATIC_1323)) | =(matching1, 0)
1305_0_growReduce_Return(EOS(STATIC_1305), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o468))) → 1325_0_growReduce_JMP(EOS(STATIC_1325)) | =(matching1, 0)
1323_0_growReduce_JMP(EOS(STATIC_1323)) → 1330_0_growReduce_Return(EOS(STATIC_1330))
1325_0_growReduce_JMP(EOS(STATIC_1325)) → 1335_0_growReduce_Return(EOS(STATIC_1335))
1371_0_growReduce_Return(EOS(STATIC_1371), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o545))))) → 1372_0_growReduce_Return(EOS(STATIC_1372), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o545))))) | =(matching1, 2)
1372_0_growReduce_Return(EOS(STATIC_1372), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o554))))) → 1383_0_growReduce_Return(EOS(STATIC_1383)) | =(matching1, 2)
1381_0_growReduce_Return(EOS(STATIC_1381), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o550))))) → 1372_0_growReduce_Return(EOS(STATIC_1372), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o550))))) | =(matching1, 2)
1402_0_growReduce_Return(EOS(STATIC_1402), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o579))) → 1403_0_growReduce_Return(EOS(STATIC_1403), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o579))) | =(matching1, 1)
1403_0_growReduce_Return(EOS(STATIC_1403), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o587))) → 1418_0_growReduce_Return(EOS(STATIC_1418)) | =(matching1, 1)
1410_0_growReduce_Return(EOS(STATIC_1410), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o583))) → 1411_0_growReduce_Return(EOS(STATIC_1411), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o583))) | =(matching1, 1)
1411_0_growReduce_Return(EOS(STATIC_1411), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o607))) → 1422_0_growReduce_Return(EOS(STATIC_1422)) | =(matching1, 1)
1456_0_growReduce_Return(EOS(STATIC_1456), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) → 1294_0_growReduce_Return(EOS(STATIC_1294), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o660))))) | =(matching1, 0)
1459_0_growReduce_Return(EOS(STATIC_1459), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) → 1305_0_growReduce_Return(EOS(STATIC_1305), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o665))))) | =(matching1, 0)
1468_0_growReduce_Return(EOS(STATIC_1468), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) → 1294_0_growReduce_Return(EOS(STATIC_1294), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o673))))) | =(matching1, 0)
1470_0_growReduce_Return(EOS(STATIC_1470), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o679))))) → 1305_0_growReduce_Return(EOS(STATIC_1305), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o679))))) | =(matching1, 0)

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

P rules:
807_0_growReduce_NONNULL(EOS(STATIC_807), 1, java.lang.Object(x1), java.lang.Object(x1)) → 1100_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(EOS(STATIC_807), 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))))
807_0_growReduce_NONNULL(EOS(STATIC_807), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1005_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(EOS(STATIC_807), 0, x1, x1), 0, x1)
807_0_growReduce_NONNULL(EOS(STATIC_807), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1008_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(EOS(STATIC_807), 0, x1, x1), 0, x1)
807_0_growReduce_NONNULL(EOS(STATIC_807), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 944_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(EOS(STATIC_807), 1, x1, x1), 1, x1)
807_0_growReduce_NONNULL(EOS(STATIC_807), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 945_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(EOS(STATIC_807), 1, x1, x1), 1, x1)
R rules:
807_0_growReduce_NONNULL(EOS(STATIC_807), x0, NULL, NULL) → 814_0_growReduce_Return(EOS(STATIC_814), x0, NULL)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), 1, NULL), 1, NULL) → 1012_0_growReduce_Return(EOS(STATIC_1012))
944_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), 1, NULL), 1, NULL) → 1012_0_growReduce_Return(EOS(STATIC_1012))
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), 0, NULL), 0, NULL) → 1129_0_growReduce_Return(EOS(STATIC_1129))
1005_1_growReduce_InvokeMethod(814_0_growReduce_Return(EOS(STATIC_814), 0, NULL), 0, NULL) → 1129_0_growReduce_Return(EOS(STATIC_1129))
1100_1_growReduce_InvokeMethod(1330_0_growReduce_Return(EOS(STATIC_1330)), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1383_0_growReduce_Return(EOS(STATIC_1383))
1100_1_growReduce_InvokeMethod(1335_0_growReduce_Return(EOS(STATIC_1335)), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1383_0_growReduce_Return(EOS(STATIC_1383))
1005_1_growReduce_InvokeMethod(1418_0_growReduce_Return(EOS(STATIC_1418)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1330_0_growReduce_Return(EOS(STATIC_1330))
1005_1_growReduce_InvokeMethod(1422_0_growReduce_Return(EOS(STATIC_1422)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1330_0_growReduce_Return(EOS(STATIC_1330))
1005_1_growReduce_InvokeMethod(1001_0_growReduce_Return(EOS(STATIC_1001)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1330_0_growReduce_Return(EOS(STATIC_1330))
1005_1_growReduce_InvokeMethod(1012_0_growReduce_Return(EOS(STATIC_1012)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1330_0_growReduce_Return(EOS(STATIC_1330))
1008_1_growReduce_InvokeMethod(1001_0_growReduce_Return(EOS(STATIC_1001)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1335_0_growReduce_Return(EOS(STATIC_1335))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return(EOS(STATIC_1012)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → 1335_0_growReduce_Return(EOS(STATIC_1335))
1008_1_growReduce_InvokeMethod(1418_0_growReduce_Return(EOS(STATIC_1418)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1335_0_growReduce_Return(EOS(STATIC_1335))
1008_1_growReduce_InvokeMethod(1422_0_growReduce_Return(EOS(STATIC_1422)), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → 1335_0_growReduce_Return(EOS(STATIC_1335))
944_1_growReduce_InvokeMethod(1383_0_growReduce_Return(EOS(STATIC_1383)), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1418_0_growReduce_Return(EOS(STATIC_1418))
945_1_growReduce_InvokeMethod(1383_0_growReduce_Return(EOS(STATIC_1383)), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → 1422_0_growReduce_Return(EOS(STATIC_1422))

Filtered ground terms:

945_1_growReduce_InvokeMethod(x1, x2, x3) → 945_1_growReduce_InvokeMethod(x1, x3)
807_0_growReduce_NONNULL(x1, x2, x3, x4) → 807_0_growReduce_NONNULL(x2, x3, x4)
AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1, x2) → AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)
944_1_growReduce_InvokeMethod(x1, x2, x3) → 944_1_growReduce_InvokeMethod(x1, x3)
1008_1_growReduce_InvokeMethod(x1, x2, x3) → 1008_1_growReduce_InvokeMethod(x1, x3)
1005_1_growReduce_InvokeMethod(x1, x2, x3) → 1005_1_growReduce_InvokeMethod(x1, x3)
1100_1_growReduce_InvokeMethod(x1, x2, x3) → 1100_1_growReduce_InvokeMethod(x1, x3)
1422_0_growReduce_Return(x1) → 1422_0_growReduce_Return
1383_0_growReduce_Return(x1) → 1383_0_growReduce_Return
1418_0_growReduce_Return(x1) → 1418_0_growReduce_Return
1335_0_growReduce_Return(x1) → 1335_0_growReduce_Return
1012_0_growReduce_Return(x1) → 1012_0_growReduce_Return
1001_0_growReduce_Return(x1) → 1001_0_growReduce_Return
1330_0_growReduce_Return(x1) → 1330_0_growReduce_Return
1129_0_growReduce_Return(x1) → 1129_0_growReduce_Return
814_0_growReduce_Return(x1, x2, x3) → 814_0_growReduce_Return(x2)

Filtered duplicate args:

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

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

P rules:
807_0_growReduce_NONNULL(1, java.lang.Object(x1)) → 1100_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1)))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
807_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1005_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(0, x1), x1)
807_0_growReduce_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1008_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(0, x1), x1)
807_0_growReduce_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 944_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(1, x1), x1)
807_0_growReduce_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 945_1_growReduce_InvokeMethod(807_0_growReduce_NONNULL(1, x1), x1)
R rules:
807_0_growReduce_NONNULL(x0, NULL) → 814_0_growReduce_Return(x0)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(1), NULL) → 1012_0_growReduce_Return
944_1_growReduce_InvokeMethod(814_0_growReduce_Return(1), NULL) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(0), NULL) → 1129_0_growReduce_Return
1005_1_growReduce_InvokeMethod(814_0_growReduce_Return(0), NULL) → 1129_0_growReduce_Return
1100_1_growReduce_InvokeMethod(1330_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1383_0_growReduce_Return
1100_1_growReduce_InvokeMethod(1335_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1383_0_growReduce_Return
1005_1_growReduce_InvokeMethod(1418_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1330_0_growReduce_Return
1005_1_growReduce_InvokeMethod(1422_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1330_0_growReduce_Return
1005_1_growReduce_InvokeMethod(1001_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1330_0_growReduce_Return
1005_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1330_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1001_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1335_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1335_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1418_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1335_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1422_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1335_0_growReduce_Return
944_1_growReduce_InvokeMethod(1383_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1418_0_growReduce_Return
945_1_growReduce_InvokeMethod(1383_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1422_0_growReduce_Return

Performed bisimulation on rules. Used the following equivalence classes: {[1008_1_growReduce_InvokeMethod_2, 1005_1_growReduce_InvokeMethod_2]=1008_1_growReduce_InvokeMethod_2, [945_1_growReduce_InvokeMethod_2, 944_1_growReduce_InvokeMethod_2]=945_1_growReduce_InvokeMethod_2, [1012_0_growReduce_Return, 1129_0_growReduce_Return, 1330_0_growReduce_Return, 1383_0_growReduce_Return, 1335_0_growReduce_Return, 1418_0_growReduce_Return, 1422_0_growReduce_Return, 1001_0_growReduce_Return]=1012_0_growReduce_Return}

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

P rules:
807_0_GROWREDUCE_NONNULL(1, java.lang.Object(x1)) → 807_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
807_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 807_0_GROWREDUCE_NONNULL(0, x1)
807_0_GROWREDUCE_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 807_0_GROWREDUCE_NONNULL(1, x1)
R rules:
807_0_growReduce_NONNULL(x0, NULL) → 814_0_growReduce_Return(x0)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(1), NULL) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(0), NULL) → 1012_0_growReduce_Return
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1012_0_growReduce_Return
945_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1012_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:
807_0_growReduce_NONNULL(x0, NULL) → 814_0_growReduce_Return(x0)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(1), NULL) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(0), NULL) → 1012_0_growReduce_Return
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1012_0_growReduce_Return
945_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1012_0_growReduce_Return

The integer pair graph contains the following rules and edges:
(0): 807_0_GROWREDUCE_NONNULL(1, java.lang.Object(x1[0])) → 807_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
(1): 807_0_GROWREDUCE_NONNULL(2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 807_0_GROWREDUCE_NONNULL(0, x1[1])
(2): 807_0_GROWREDUCE_NONNULL(0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 807_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:
807_0_growReduce_NONNULL(x0, NULL)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(1), NULL)
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(0), NULL)
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
945_1_growReduce_InvokeMethod(1012_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:

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

The TRS R consists of the following rules:

807_0_growReduce_NONNULL(x0, NULL) → 814_0_growReduce_Return(x0)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(s(01))), NULL) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(01)), NULL) → 1012_0_growReduce_Return
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))))) → 1012_0_growReduce_Return
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL))) → 1012_0_growReduce_Return
945_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → 1012_0_growReduce_Return

The set Q consists of the following terms:

807_0_growReduce_NONNULL(x0, NULL)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(s(01))), NULL)
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(01)), NULL)
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
945_1_growReduce_InvokeMethod(1012_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:

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

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

807_0_growReduce_NONNULL(x0, NULL)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(s(01))), NULL)
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(01)), NULL)
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
945_1_growReduce_InvokeMethod(1012_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].

807_0_growReduce_NONNULL(x0, NULL)
945_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(s(01))), NULL)
1008_1_growReduce_InvokeMethod(814_0_growReduce_Return(pos(01)), NULL)
1100_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))))
1008_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(NULL)))
945_1_growReduce_InvokeMethod(1012_0_growReduce_Return, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x0)))

(13) Obligation:

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

807_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 807_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
807_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 807_0_GROWREDUCE_NONNULL(pos(01), x1[1])
807_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 807_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.

807_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[1]))) → 807_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(807_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:

807_0_GROWREDUCE_NONNULL(pos(s(01)), java.lang.Object(x1[0])) → 807_0_GROWREDUCE_NONNULL(pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[0]))))
807_0_GROWREDUCE_NONNULL(pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[2]))) → 807_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:
172_0_createList_Duplicate(EOS(STATIC_172), i18) → 177_0_createList_ConstantStackPush(EOS(STATIC_177), i18)
177_0_createList_ConstantStackPush(EOS(STATIC_177), i18) → 184_0_createList_InvokeMethod(EOS(STATIC_184), i18)
184_0_createList_InvokeMethod(EOS(STATIC_184), i18) → 191_0_<init>_Load(EOS(STATIC_191), i18)
191_0_<init>_Load(EOS(STATIC_191), i18) → 202_0_<init>_InvokeMethod(EOS(STATIC_202), i18)
202_0_<init>_InvokeMethod(EOS(STATIC_202), i18) → 213_0_<init>_Load(EOS(STATIC_213), i18)
213_0_<init>_Load(EOS(STATIC_213), i18) → 219_0_<init>_Load(EOS(STATIC_219), i18)
219_0_<init>_Load(EOS(STATIC_219), i18) → 223_0_<init>_FieldAccess(EOS(STATIC_223), i18)
223_0_<init>_FieldAccess(EOS(STATIC_223), i18) → 228_0_<init>_Return(EOS(STATIC_228), i18)
228_0_<init>_Return(EOS(STATIC_228), i18) → 230_0_createList_Store(EOS(STATIC_230), i18)
230_0_createList_Store(EOS(STATIC_230), i18) → 232_0_createList_Load(EOS(STATIC_232), i18)
232_0_createList_Load(EOS(STATIC_232), i18) → 234_0_createList_ConstantStackPush(EOS(STATIC_234), i18, i18)
234_0_createList_ConstantStackPush(EOS(STATIC_234), i18, i18) → 241_0_createList_LE(EOS(STATIC_241), i18, i18, 1)
241_0_createList_LE(EOS(STATIC_241), i26, i26, matching1) → 247_0_createList_LE(EOS(STATIC_247), i26, i26, 1) | =(matching1, 1)
247_0_createList_LE(EOS(STATIC_247), i26, i26, matching1) → 253_0_createList_Load(EOS(STATIC_253), i26) | &&(>(i26, 1), =(matching1, 1))
253_0_createList_Load(EOS(STATIC_253), i26) → 257_0_createList_Load(EOS(STATIC_257), i26)
257_0_createList_Load(EOS(STATIC_257), i26) → 263_0_createList_ConstantStackPush(EOS(STATIC_263), i26)
263_0_createList_ConstantStackPush(EOS(STATIC_263), i26) → 276_0_createList_IntArithmetic(EOS(STATIC_276), i26, 1)
276_0_createList_IntArithmetic(EOS(STATIC_276), i26, matching1) → 280_0_createList_InvokeMethod(EOS(STATIC_280), -(i26, 1)) | &&(>(i26, 0), =(matching1, 1))
280_0_createList_InvokeMethod(EOS(STATIC_280), i31) → 284_1_createList_InvokeMethod(284_0_createList_New(EOS(STATIC_284), i31), i31)
284_0_createList_New(EOS(STATIC_284), i31) → 289_0_createList_New(EOS(STATIC_289), i31)
289_0_createList_New(EOS(STATIC_289), i31) → 166_0_createList_New(EOS(STATIC_166), i31)
166_0_createList_New(EOS(STATIC_166), i18) → 172_0_createList_Duplicate(EOS(STATIC_172), i18)
R rules:
241_0_createList_LE(EOS(STATIC_241), i25, i25, matching1) → 246_0_createList_LE(EOS(STATIC_246), i25, i25, 1) | =(matching1, 1)
246_0_createList_LE(EOS(STATIC_246), i25, i25, matching1) → 251_0_createList_Load(EOS(STATIC_251)) | &&(<=(i25, 1), =(matching1, 1))
251_0_createList_Load(EOS(STATIC_251)) → 255_0_createList_Return(EOS(STATIC_255))
284_1_createList_InvokeMethod(255_0_createList_Return(EOS(STATIC_255)), matching1) → 305_0_createList_Return(EOS(STATIC_305), 1) | =(matching1, 1)
284_1_createList_InvokeMethod(379_0_createList_Return(EOS(STATIC_379)), i53) → 412_0_createList_Return(EOS(STATIC_412), i53)
305_0_createList_Return(EOS(STATIC_305), matching1) → 359_0_createList_Return(EOS(STATIC_359), 1) | =(matching1, 1)
359_0_createList_Return(EOS(STATIC_359), i46) → 365_0_createList_FieldAccess(EOS(STATIC_365))
365_0_createList_FieldAccess(EOS(STATIC_365)) → 372_0_createList_Load(EOS(STATIC_372))
372_0_createList_Load(EOS(STATIC_372)) → 379_0_createList_Return(EOS(STATIC_379))
412_0_createList_Return(EOS(STATIC_412), i53) → 359_0_createList_Return(EOS(STATIC_359), i53)

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

P rules:
172_0_createList_Duplicate(EOS(STATIC_172), x0) → 284_1_createList_InvokeMethod(172_0_createList_Duplicate(EOS(STATIC_172), -(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
284_1_createList_InvokeMethod(255_0_createList_Return(EOS(STATIC_255)), 1) → 379_0_createList_Return(EOS(STATIC_379))
284_1_createList_InvokeMethod(379_0_createList_Return(EOS(STATIC_379)), x0) → 379_0_createList_Return(EOS(STATIC_379))

Filtered ground terms:

172_0_createList_Duplicate(x1, x2) → 172_0_createList_Duplicate(x2)
Cond_172_0_createList_Duplicate(x1, x2, x3) → Cond_172_0_createList_Duplicate(x1, x3)
379_0_createList_Return(x1) → 379_0_createList_Return
255_0_createList_Return(x1) → 255_0_createList_Return

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

P rules:
172_0_createList_Duplicate(x0) → 284_1_createList_InvokeMethod(172_0_createList_Duplicate(-(x0, 1)), -(x0, 1)) | >(x0, 1)
R rules:
284_1_createList_InvokeMethod(255_0_createList_Return, 1) → 379_0_createList_Return
284_1_createList_InvokeMethod(379_0_createList_Return, x0) → 379_0_createList_Return

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

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

P rules:
172_0_CREATELIST_DUPLICATE(x0) → COND_172_0_CREATELIST_DUPLICATE(>(x0, 1), x0)
COND_172_0_CREATELIST_DUPLICATE(TRUE, x0) → 172_0_CREATELIST_DUPLICATE(-(x0, 1))
R rules:
284_1_createList_InvokeMethod(255_0_createList_Return, 1) → 255_0_createList_Return
284_1_createList_InvokeMethod(255_0_createList_Return, x0) → 255_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:
284_1_createList_InvokeMethod(255_0_createList_Return, 1) → 255_0_createList_Return
284_1_createList_InvokeMethod(255_0_createList_Return, x0) → 255_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 172_0_CREATELIST_DUPLICATE(x0[0]) → COND_172_0_CREATELIST_DUPLICATE(x0[0] > 1, x0[0])
(1): COND_172_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 172_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:
284_1_createList_InvokeMethod(255_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@4c66f067 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 172_0_CREATELIST_DUPLICATE(x0) → COND_172_0_CREATELIST_DUPLICATE(>(x0, 1), x0) the following chains were created:

We consider the chain 172_0_CREATELIST_DUPLICATE(x0[0]) → COND_172_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0]), COND_172_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 172_0_CREATELIST_DUPLICATE(-(x0[1], 1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 172_0_CREATELIST_DUPLICATE(x0[0])≥NonInfC∧172_0_CREATELIST_DUPLICATE(x0[0])≥COND_172_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])∧(U^Increasing(COND_172_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 ⇒ 172_0_CREATELIST_DUPLICATE(x0[0])≥NonInfC∧172_0_CREATELIST_DUPLICATE(x0[0])≥COND_172_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])∧(U^Increasing(COND_172_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_172_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_172_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_172_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_172_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_172_0_CREATELIST_DUPLICATE(TRUE, x0) → 172_0_CREATELIST_DUPLICATE(-(x0, 1)) the following chains were created:

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

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(172_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(172_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(172_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(172_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.

172_0_CREATELIST_DUPLICATE(x0) → COND_172_0_CREATELIST_DUPLICATE(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_172_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_172_0_CREATELIST_DUPLICATE(TRUE, x0) → 172_0_CREATELIST_DUPLICATE(-(x0, 1))
- ((U^Increasing(172_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(284_1_createList_InvokeMethod(x₁, x₂)) = [-1]
POL(255_0_createList_Return) = [-1]
POL(1) = [1]
POL(172_0_CREATELIST_DUPLICATE(x₁)) = [2]x₁
POL(COND_172_0_CREATELIST_DUPLICATE(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂

The following pairs are in P_>:

COND_172_0_CREATELIST_DUPLICATE(TRUE, x0[1]) → 172_0_CREATELIST_DUPLICATE(-(x0[1], 1))

The following pairs are in P_bound:

172_0_CREATELIST_DUPLICATE(x0[0]) → COND_172_0_CREATELIST_DUPLICATE(>(x0[0], 1), x0[0])

The following pairs are in P_≥:

172_0_CREATELIST_DUPLICATE(x0[0]) → COND_172_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:
284_1_createList_InvokeMethod(255_0_createList_Return, 1) → 255_0_createList_Return
284_1_createList_InvokeMethod(255_0_createList_Return, x0) → 255_0_createList_Return

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

The set Q consists of the following terms:
284_1_createList_InvokeMethod(255_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:
284_1_createList_InvokeMethod(255_0_createList_Return, 1) → 255_0_createList_Return
284_1_createList_InvokeMethod(255_0_createList_Return, x0) → 255_0_createList_Return

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

The set Q consists of the following terms:
284_1_createList_InvokeMethod(255_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