Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 1144 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIDPv1Proof (⇒, 595 ms)
        ↳7 IDP
        ↳8 IDPtoQDPProof (⇒, 0 ms)
        ↳9 QDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPQMonotonicMRRProof (⇔, 205 ms)
        ↳13 QDP
        ↳14 QDPQMonotonicMRRProof (⇔, 211 ms)
        ↳15 QDP
        ↳16 QDPQMonotonicMRRProof (⇔, 150 ms)
        ↳17 QDP
        ↳18 QDPQMonotonicMRRProof (⇔, 46 ms)
        ↳19 QDP
        ↳20 QDPQMonotonicMRRProof (⇔, 140 ms)
        ↳21 QDP
        ↳22 QDPQMonotonicMRRProof (⇔, 147 ms)
        ↳23 QDP
        ↳24 QDPQMonotonicMRRProof (⇔, 128 ms)
        ↳25 QDP
        ↳26 QDPQMonotonicMRRProof (⇔, 127 ms)
        ↳27 QDP
        ↳28 QDPOrderProof (⇔, 25 ms)
        ↳29 QDP
        ↳30 DependencyGraphProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 UsableRulesProof (⇔, 0 ms)
        ↳33 QDP
        ↳34 QReductionProof (⇔, 0 ms)
        ↳35 QDP
        ↳36 Instantiation (⇔, 0 ms)
        ↳37 QDP
        ↳38 DependencyGraphProof (⇔, 0 ms)
        ↳39 QDP
        ↳40 Rewriting (⇔, 0 ms)
        ↳41 QDP
        ↳42 Rewriting (⇔, 0 ms)
        ↳43 QDP
        ↳44 DependencyGraphProof (⇔, 0 ms)
        ↳45 QDP
        ↳46 UsableRulesProof (⇔, 0 ms)
        ↳47 QDP
        ↳48 Rewriting (⇔, 0 ms)
        ↳49 QDP
        ↳50 UsableRulesProof (⇔, 0 ms)
        ↳51 QDP
        ↳52 QReductionProof (⇔, 0 ms)
        ↳53 QDP
        ↳54 Instantiation (⇔, 0 ms)
        ↳55 QDP
        ↳56 Instantiation (⇔, 0 ms)
        ↳57 QDP
        ↳58 DependencyGraphProof (⇔, 0 ms)
        ↳59 TRUE
    ↳60 JBCTerminationSCC
        ↳61 SCCToIntTRSProof (⇒, 88 ms)
        ↳62 intTRS
        ↳63 PolynomialOrderProcessor (⇔, 0 ms)
        ↳64 YES

(0) Obligation:

JBC Problem based on JBC Program:
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 113 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 121 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:
  • Used field analysis yielded the following read fields:
    • AlternatingGrowReduceRec2.AlternatingGrowReduceRec2: [next]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 84 rules for P and 126 rules for R.


P rules:
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub)) → f2080_0_growReduce_NONNULL(EOS(STATIC_2080), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub))
f2080_0_growReduce_NONNULL(EOS(STATIC_2080), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub)) → f2083_0_growReduce_Load(EOS(STATIC_2083), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub))
f2083_0_growReduce_Load(EOS(STATIC_2083), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub)) → f2086_0_growReduce_NE(EOS(STATIC_2086), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), i239)
f2086_0_growReduce_NE(EOS(STATIC_2086), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2090_0_growReduce_NE(EOS(STATIC_2090), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305)
f2086_0_growReduce_NE(EOS(STATIC_2086), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3) → f2091_0_growReduce_NE(EOS(STATIC_2091), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub), 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f2090_0_growReduce_NE(EOS(STATIC_2090), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2097_0_growReduce_Load(EOS(STATIC_2097), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub)) | !(=(i305, 0))
f2097_0_growReduce_Load(EOS(STATIC_2097), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub)) → f2101_0_growReduce_ConstantStackPush(EOS(STATIC_2101), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305)
f2101_0_growReduce_ConstantStackPush(EOS(STATIC_2101), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2106_0_growReduce_NE(EOS(STATIC_2106), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305, 1)
f2106_0_growReduce_NE(EOS(STATIC_2106), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2111_0_growReduce_NE(EOS(STATIC_2111), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, 1) | =(matching1, 1)
f2106_0_growReduce_NE(EOS(STATIC_2106), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3, matching4) → f2112_0_growReduce_NE(EOS(STATIC_2112), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), 1, 1) | &&(&&(&&(&&(=(i305, 1), =(matching1, 1)), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
f2106_0_growReduce_NE(EOS(STATIC_2106), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2113_0_growReduce_NE(EOS(STATIC_2113), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, 1) | =(matching1, 1)
f2111_0_growReduce_NE(EOS(STATIC_2111), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2117_0_growReduce_Load(EOS(STATIC_2117), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) | &&(<(i312, 1), =(matching1, 1))
f2117_0_growReduce_Load(EOS(STATIC_2117), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) → f2122_0_growReduce_ConstantStackPush(EOS(STATIC_2122), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312)
f2122_0_growReduce_ConstantStackPush(EOS(STATIC_2122), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312) → f2130_0_growReduce_LE(EOS(STATIC_2130), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, 1)
f2130_0_growReduce_LE(EOS(STATIC_2130), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2138_0_growReduce_Inc(EOS(STATIC_2138), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) | &&(<=(i312, 1), =(matching1, 1))
f2138_0_growReduce_Inc(EOS(STATIC_2138), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) → f2144_0_growReduce_Load(EOS(STATIC_2144), i312, java.lang.Object(o878sub), o533, +(i312, 1), java.lang.Object(o878sub)) | <(i312, 0)
f2144_0_growReduce_Load(EOS(STATIC_2144), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2152_0_growReduce_ConstantStackPush(EOS(STATIC_2152), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314)
f2152_0_growReduce_ConstantStackPush(EOS(STATIC_2152), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314) → f2156_0_growReduce_LE(EOS(STATIC_2156), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314, 2)
f2156_0_growReduce_LE(EOS(STATIC_2156), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314, matching1) → f2163_0_growReduce_Load(EOS(STATIC_2163), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) | &&(<=(i314, 2), =(matching1, 2))
f2163_0_growReduce_Load(EOS(STATIC_2163), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2172_0_growReduce_Load(EOS(STATIC_2172), i312, java.lang.Object(o878sub), o533, java.lang.Object(o878sub), i314)
f2172_0_growReduce_Load(EOS(STATIC_2172), i312, java.lang.Object(o878sub), o533, java.lang.Object(o878sub), i314) → f2178_0_growReduce_InvokeMethod(EOS(STATIC_2178), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2178_0_growReduce_InvokeMethod(EOS(STATIC_2178), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2186_1_growReduce_InvokeMethod(f2186_0_growReduce_Load(EOS(STATIC_2186), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2186_0_growReduce_Load(EOS(STATIC_2186), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2200_0_growReduce_Load(EOS(STATIC_2200), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2200_0_growReduce_Load(EOS(STATIC_2200), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2075_0_growReduce_Load(EOS(STATIC_2075), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2075_0_growReduce_Load(EOS(STATIC_2075), i239, o532, o533, i239, o532) → f2078_0_growReduce_NONNULL(EOS(STATIC_2078), i239, o532, o533, i239, o532, o532)
f2112_0_growReduce_NE(EOS(STATIC_2112), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3, matching4) → f2118_0_growReduce_New(EOS(STATIC_2118), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub)) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
f2118_0_growReduce_New(EOS(STATIC_2118), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub)) → f2124_0_growReduce_Duplicate(EOS(STATIC_2124), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2124_0_growReduce_Duplicate(EOS(STATIC_2124), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2131_0_growReduce_Load(EOS(STATIC_2131), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2131_0_growReduce_Load(EOS(STATIC_2131), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2139_0_growReduce_InvokeMethod(EOS(STATIC_2139), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2139_0_growReduce_InvokeMethod(EOS(STATIC_2139), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2146_0__init__Load(EOS(STATIC_2146), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2146_0__init__Load(EOS(STATIC_2146), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2157_0__init__InvokeMethod(EOS(STATIC_2157), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2157_0__init__InvokeMethod(EOS(STATIC_2157), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2165_0__init__Load(EOS(STATIC_2165), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2165_0__init__Load(EOS(STATIC_2165), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2173_0__init__Load(EOS(STATIC_2173), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2173_0__init__Load(EOS(STATIC_2173), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2179_0__init__FieldAccess(EOS(STATIC_2179), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2179_0__init__FieldAccess(EOS(STATIC_2179), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2190_0__init__Return(EOS(STATIC_2190), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2190_0__init__Return(EOS(STATIC_2190), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(o878sub)) → f2201_0_growReduce_Store(EOS(STATIC_2201), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2201_0_growReduce_Store(EOS(STATIC_2201), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2210_0_growReduce_JMP(EOS(STATIC_2210), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2210_0_growReduce_JMP(EOS(STATIC_2210), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2233_0_growReduce_Inc(EOS(STATIC_2233), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2233_0_growReduce_Inc(EOS(STATIC_2233), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2240_0_growReduce_Load(EOS(STATIC_2240), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2240_0_growReduce_Load(EOS(STATIC_2240), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2248_0_growReduce_ConstantStackPush(EOS(STATIC_2248), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2) | &&(=(matching1, 1), =(matching2, 2))
f2248_0_growReduce_ConstantStackPush(EOS(STATIC_2248), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching3) → f2254_0_growReduce_LE(EOS(STATIC_2254), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2, 2) | &&(&&(=(matching1, 1), =(matching2, 2)), =(matching3, 2))
f2254_0_growReduce_LE(EOS(STATIC_2254), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching3, matching4) → f2285_0_growReduce_Load(EOS(STATIC_2285), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(&&(&&(=(matching1, 1), =(matching2, 2)), =(matching3, 2)), =(matching4, 2))
f2285_0_growReduce_Load(EOS(STATIC_2285), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2294_0_growReduce_Load(EOS(STATIC_2294), 1, java.lang.Object(o878sub), o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2) | &&(=(matching1, 1), =(matching2, 2))
f2294_0_growReduce_Load(EOS(STATIC_2294), matching1, java.lang.Object(o878sub), o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching2) → f2323_0_growReduce_InvokeMethod(EOS(STATIC_2323), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 2))
f2323_0_growReduce_InvokeMethod(EOS(STATIC_2323), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2330_1_growReduce_InvokeMethod(f2330_0_growReduce_Load(EOS(STATIC_2330), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 2))
f2330_0_growReduce_Load(EOS(STATIC_2330), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2404_0_growReduce_Load(EOS(STATIC_2404), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 2), =(matching2, 2))
f2404_0_growReduce_Load(EOS(STATIC_2404), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2465_0_growReduce_Load(EOS(STATIC_2465), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 2), =(matching2, 2))
f2465_0_growReduce_Load(EOS(STATIC_2465), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533))) → f2075_0_growReduce_Load(EOS(STATIC_2075), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533)), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533))) | &&(=(matching1, 2), =(matching2, 2))
f2113_0_growReduce_NE(EOS(STATIC_2113), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2119_0_growReduce_Load(EOS(STATIC_2119), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) | &&(>(i313, 1), =(matching1, 1))
f2119_0_growReduce_Load(EOS(STATIC_2119), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) → f2126_0_growReduce_ConstantStackPush(EOS(STATIC_2126), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313)
f2126_0_growReduce_ConstantStackPush(EOS(STATIC_2126), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313) → f2133_0_growReduce_LE(EOS(STATIC_2133), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, 1)
f2133_0_growReduce_LE(EOS(STATIC_2133), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2141_0_growReduce_Load(EOS(STATIC_2141), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) | &&(>(i313, 1), =(matching1, 1))
f2141_0_growReduce_Load(EOS(STATIC_2141), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) → f2148_0_growReduce_FieldAccess(EOS(STATIC_2148), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub))
f2148_0_growReduce_FieldAccess(EOS(STATIC_2148), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896))) → f2153_0_growReduce_FieldAccess(EOS(STATIC_2153), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)))
f2153_0_growReduce_FieldAccess(EOS(STATIC_2153), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896))) → f2159_0_growReduce_Store(EOS(STATIC_2159), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896)
f2159_0_growReduce_Store(EOS(STATIC_2159), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896) → f2168_0_growReduce_Inc(EOS(STATIC_2168), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896)
f2168_0_growReduce_Inc(EOS(STATIC_2168), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896) → f2175_0_growReduce_Load(EOS(STATIC_2175), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, +(i313, 1), o896) | >(i313, 0)
f2175_0_growReduce_Load(EOS(STATIC_2175), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896) → f2183_0_growReduce_ConstantStackPush(EOS(STATIC_2183), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315)
f2183_0_growReduce_ConstantStackPush(EOS(STATIC_2183), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315) → f2193_0_growReduce_LE(EOS(STATIC_2193), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315, 2)
f2193_0_growReduce_LE(EOS(STATIC_2193), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315, matching1) → f2203_0_growReduce_ConstantStackPush(EOS(STATIC_2203), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896) | &&(>(i315, 2), =(matching1, 2))
f2203_0_growReduce_ConstantStackPush(EOS(STATIC_2203), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896) → f2211_0_growReduce_Load(EOS(STATIC_2211), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896, 0)
f2211_0_growReduce_Load(EOS(STATIC_2211), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896, matching1) → f2235_0_growReduce_InvokeMethod(EOS(STATIC_2235), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, 0, o896) | =(matching1, 0)
f2235_0_growReduce_InvokeMethod(EOS(STATIC_2235), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, matching1, o896) → f2242_1_growReduce_InvokeMethod(f2242_0_growReduce_Load(EOS(STATIC_2242), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, 0, o896) | =(matching1, 0)
f2242_0_growReduce_Load(EOS(STATIC_2242), matching1, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), matching2, o896) → f2250_0_growReduce_Load(EOS(STATIC_2250), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896) | &&(=(matching1, 0), =(matching2, 0))
f2250_0_growReduce_Load(EOS(STATIC_2250), matching1, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), matching2, o896) → f2260_0_growReduce_Load(EOS(STATIC_2260), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896) | &&(=(matching1, 0), =(matching2, 0))
f2260_0_growReduce_Load(EOS(STATIC_2260), matching1, o965, o966, o968, matching2, o965) → f2289_0_growReduce_Load(EOS(STATIC_2289), 0, o965, o966, 0, o965) | &&(=(matching1, 0), =(matching2, 0))
f2289_0_growReduce_Load(EOS(STATIC_2289), matching1, o965, o966, matching2, o965) → f2075_0_growReduce_Load(EOS(STATIC_2075), 0, o965, o966, 0, o965) | &&(=(matching1, 0), =(matching2, 0))
f2091_0_growReduce_NE(EOS(STATIC_2091), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3) → f2100_0_growReduce_Load(EOS(STATIC_2100), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub)) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f2100_0_growReduce_Load(EOS(STATIC_2100), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub)) → f2104_0_growReduce_FieldAccess(EOS(STATIC_2104), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub)) | &&(=(matching1, 0), =(matching2, 0))
f2104_0_growReduce_FieldAccess(EOS(STATIC_2104), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) → f2108_0_growReduce_FieldAccess(EOS(STATIC_2108), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) | &&(=(matching1, 0), =(matching2, 0))
f2108_0_growReduce_FieldAccess(EOS(STATIC_2108), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) → f2116_0_growReduce_Store(EOS(STATIC_2116), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2116_0_growReduce_Store(EOS(STATIC_2116), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2120_0_growReduce_JMP(EOS(STATIC_2120), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2120_0_growReduce_JMP(EOS(STATIC_2120), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2128_0_growReduce_Inc(EOS(STATIC_2128), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2128_0_growReduce_Inc(EOS(STATIC_2128), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2135_0_growReduce_Load(EOS(STATIC_2135), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 0))
f2135_0_growReduce_Load(EOS(STATIC_2135), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2142_0_growReduce_ConstantStackPush(EOS(STATIC_2142), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885, 1) | &&(=(matching1, 0), =(matching2, 1))
f2142_0_growReduce_ConstantStackPush(EOS(STATIC_2142), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885, matching3) → f2150_0_growReduce_LE(EOS(STATIC_2150), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885, 1) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 1))
f2150_0_growReduce_LE(EOS(STATIC_2150), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885, matching3) → f2154_0_growReduce_Load(EOS(STATIC_2154), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 1))
f2154_0_growReduce_Load(EOS(STATIC_2154), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2161_0_growReduce_Load(EOS(STATIC_2161), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, o885, 1) | &&(=(matching1, 0), =(matching2, 1))
f2161_0_growReduce_Load(EOS(STATIC_2161), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, o885, matching2) → f2169_0_growReduce_InvokeMethod(EOS(STATIC_2169), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 1))
f2169_0_growReduce_InvokeMethod(EOS(STATIC_2169), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2176_1_growReduce_InvokeMethod(f2176_0_growReduce_Load(EOS(STATIC_2176), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 1))
f2176_0_growReduce_Load(EOS(STATIC_2176), matching1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), matching2, o885) → f2185_0_growReduce_Load(EOS(STATIC_2185), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885) | &&(=(matching1, 1), =(matching2, 1))
f2185_0_growReduce_Load(EOS(STATIC_2185), matching1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), matching2, o885) → f2198_0_growReduce_Load(EOS(STATIC_2198), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885) | &&(=(matching1, 1), =(matching2, 1))
f2198_0_growReduce_Load(EOS(STATIC_2198), matching1, o911, o912, o914, matching2, o911) → f2208_0_growReduce_Load(EOS(STATIC_2208), 1, o911, o912, 1, o911) | &&(=(matching1, 1), =(matching2, 1))
f2208_0_growReduce_Load(EOS(STATIC_2208), matching1, o911, o912, matching2, o911) → f2075_0_growReduce_Load(EOS(STATIC_2075), 1, o911, o912, 1, o911) | &&(=(matching1, 1), =(matching2, 1))
R rules:
f2075_0_growReduce_Load(EOS(STATIC_2075), i239, o532, o533, i239, o532) → f2078_0_growReduce_NONNULL(EOS(STATIC_2078), i239, o532, o533, i239, o532, o532)
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub)) → f2080_0_growReduce_NONNULL(EOS(STATIC_2080), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub))
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), i239, NULL, o533, i239, NULL, NULL) → f2081_0_growReduce_NONNULL(EOS(STATIC_2081), i239, NULL, o533, i239, NULL, NULL)
f2080_0_growReduce_NONNULL(EOS(STATIC_2080), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), java.lang.Object(o878sub)) → f2083_0_growReduce_Load(EOS(STATIC_2083), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub))
f2081_0_growReduce_NONNULL(EOS(STATIC_2081), i239, NULL, o533, i239, NULL, NULL) → f2085_0_growReduce_Return(EOS(STATIC_2085), i239, NULL, o533, i239, NULL)
f2083_0_growReduce_Load(EOS(STATIC_2083), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub)) → f2086_0_growReduce_NE(EOS(STATIC_2086), i239, java.lang.Object(o878sub), o533, i239, java.lang.Object(o878sub), i239)
f2086_0_growReduce_NE(EOS(STATIC_2086), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2090_0_growReduce_NE(EOS(STATIC_2090), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305)
f2086_0_growReduce_NE(EOS(STATIC_2086), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3) → f2091_0_growReduce_NE(EOS(STATIC_2091), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub), 0) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f2090_0_growReduce_NE(EOS(STATIC_2090), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2097_0_growReduce_Load(EOS(STATIC_2097), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub)) | !(=(i305, 0))
f2091_0_growReduce_NE(EOS(STATIC_2091), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3) → f2100_0_growReduce_Load(EOS(STATIC_2100), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub)) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f2097_0_growReduce_Load(EOS(STATIC_2097), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub)) → f2101_0_growReduce_ConstantStackPush(EOS(STATIC_2101), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305)
f2100_0_growReduce_Load(EOS(STATIC_2100), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub)) → f2104_0_growReduce_FieldAccess(EOS(STATIC_2104), 0, java.lang.Object(o878sub), o533, 0, java.lang.Object(o878sub)) | &&(=(matching1, 0), =(matching2, 0))
f2101_0_growReduce_ConstantStackPush(EOS(STATIC_2101), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305) → f2106_0_growReduce_NE(EOS(STATIC_2106), i305, java.lang.Object(o878sub), o533, i305, java.lang.Object(o878sub), i305, 1)
f2104_0_growReduce_FieldAccess(EOS(STATIC_2104), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) → f2108_0_growReduce_FieldAccess(EOS(STATIC_2108), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) | &&(=(matching1, 0), =(matching2, 0))
f2106_0_growReduce_NE(EOS(STATIC_2106), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2111_0_growReduce_NE(EOS(STATIC_2111), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, 1) | =(matching1, 1)
f2106_0_growReduce_NE(EOS(STATIC_2106), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3, matching4) → f2112_0_growReduce_NE(EOS(STATIC_2112), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), 1, 1) | &&(&&(&&(&&(=(i305, 1), =(matching1, 1)), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
f2106_0_growReduce_NE(EOS(STATIC_2106), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2113_0_growReduce_NE(EOS(STATIC_2113), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, 1) | =(matching1, 1)
f2108_0_growReduce_FieldAccess(EOS(STATIC_2108), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885))) → f2116_0_growReduce_Store(EOS(STATIC_2116), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2111_0_growReduce_NE(EOS(STATIC_2111), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2117_0_growReduce_Load(EOS(STATIC_2117), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) | &&(<(i312, 1), =(matching1, 1))
f2112_0_growReduce_NE(EOS(STATIC_2112), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), matching3, matching4) → f2118_0_growReduce_New(EOS(STATIC_2118), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub)) | &&(&&(&&(=(matching1, 1), =(matching2, 1)), =(matching3, 1)), =(matching4, 1))
f2113_0_growReduce_NE(EOS(STATIC_2113), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2119_0_growReduce_Load(EOS(STATIC_2119), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) | &&(>(i313, 1), =(matching1, 1))
f2116_0_growReduce_Store(EOS(STATIC_2116), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2120_0_growReduce_JMP(EOS(STATIC_2120), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2117_0_growReduce_Load(EOS(STATIC_2117), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) → f2122_0_growReduce_ConstantStackPush(EOS(STATIC_2122), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312)
f2118_0_growReduce_New(EOS(STATIC_2118), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub)) → f2124_0_growReduce_Duplicate(EOS(STATIC_2124), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2119_0_growReduce_Load(EOS(STATIC_2119), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) → f2126_0_growReduce_ConstantStackPush(EOS(STATIC_2126), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313)
f2120_0_growReduce_JMP(EOS(STATIC_2120), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2128_0_growReduce_Inc(EOS(STATIC_2128), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 0, o885) | &&(=(matching1, 0), =(matching2, 0))
f2122_0_growReduce_ConstantStackPush(EOS(STATIC_2122), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312) → f2130_0_growReduce_LE(EOS(STATIC_2130), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, 1)
f2124_0_growReduce_Duplicate(EOS(STATIC_2124), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2131_0_growReduce_Load(EOS(STATIC_2131), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2126_0_growReduce_ConstantStackPush(EOS(STATIC_2126), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313) → f2133_0_growReduce_LE(EOS(STATIC_2133), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, 1)
f2128_0_growReduce_Inc(EOS(STATIC_2128), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2135_0_growReduce_Load(EOS(STATIC_2135), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 0))
f2130_0_growReduce_LE(EOS(STATIC_2130), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub), i312, matching1) → f2138_0_growReduce_Inc(EOS(STATIC_2138), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) | &&(<=(i312, 1), =(matching1, 1))
f2131_0_growReduce_Load(EOS(STATIC_2131), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2139_0_growReduce_InvokeMethod(EOS(STATIC_2139), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2133_0_growReduce_LE(EOS(STATIC_2133), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub), i313, matching1) → f2141_0_growReduce_Load(EOS(STATIC_2141), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) | &&(>(i313, 1), =(matching1, 1))
f2135_0_growReduce_Load(EOS(STATIC_2135), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2142_0_growReduce_ConstantStackPush(EOS(STATIC_2142), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885, 1) | &&(=(matching1, 0), =(matching2, 1))
f2138_0_growReduce_Inc(EOS(STATIC_2138), i312, java.lang.Object(o878sub), o533, i312, java.lang.Object(o878sub)) → f2144_0_growReduce_Load(EOS(STATIC_2144), i312, java.lang.Object(o878sub), o533, +(i312, 1), java.lang.Object(o878sub)) | <(i312, 0)
f2139_0_growReduce_InvokeMethod(EOS(STATIC_2139), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2146_0__init__Load(EOS(STATIC_2146), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2141_0_growReduce_Load(EOS(STATIC_2141), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub)) → f2148_0_growReduce_FieldAccess(EOS(STATIC_2148), i313, java.lang.Object(o878sub), o533, i313, java.lang.Object(o878sub))
f2142_0_growReduce_ConstantStackPush(EOS(STATIC_2142), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885, matching3) → f2150_0_growReduce_LE(EOS(STATIC_2150), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885, 1) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 1))
f2144_0_growReduce_Load(EOS(STATIC_2144), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2152_0_growReduce_ConstantStackPush(EOS(STATIC_2152), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314)
f2146_0__init__Load(EOS(STATIC_2146), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2157_0__init__InvokeMethod(EOS(STATIC_2157), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2148_0_growReduce_FieldAccess(EOS(STATIC_2148), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896))) → f2153_0_growReduce_FieldAccess(EOS(STATIC_2153), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)))
f2150_0_growReduce_LE(EOS(STATIC_2150), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885, matching3) → f2154_0_growReduce_Load(EOS(STATIC_2154), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 1))
f2152_0_growReduce_ConstantStackPush(EOS(STATIC_2152), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314) → f2156_0_growReduce_LE(EOS(STATIC_2156), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314, 2)
f2153_0_growReduce_FieldAccess(EOS(STATIC_2153), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896))) → f2159_0_growReduce_Store(EOS(STATIC_2159), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896)
f2154_0_growReduce_Load(EOS(STATIC_2154), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2161_0_growReduce_Load(EOS(STATIC_2161), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, o885, 1) | &&(=(matching1, 0), =(matching2, 1))
f2156_0_growReduce_LE(EOS(STATIC_2156), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub), i314, matching1) → f2163_0_growReduce_Load(EOS(STATIC_2163), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) | &&(<=(i314, 2), =(matching1, 2))
f2157_0__init__InvokeMethod(EOS(STATIC_2157), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2165_0__init__Load(EOS(STATIC_2165), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2159_0_growReduce_Store(EOS(STATIC_2159), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896) → f2168_0_growReduce_Inc(EOS(STATIC_2168), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896)
f2161_0_growReduce_Load(EOS(STATIC_2161), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, o885, matching2) → f2169_0_growReduce_InvokeMethod(EOS(STATIC_2169), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 1))
f2163_0_growReduce_Load(EOS(STATIC_2163), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2172_0_growReduce_Load(EOS(STATIC_2172), i312, java.lang.Object(o878sub), o533, java.lang.Object(o878sub), i314)
f2165_0__init__Load(EOS(STATIC_2165), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2173_0__init__Load(EOS(STATIC_2173), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 1), =(matching2, 1))
f2168_0_growReduce_Inc(EOS(STATIC_2168), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i313, o896) → f2175_0_growReduce_Load(EOS(STATIC_2175), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, +(i313, 1), o896) | >(i313, 0)
f2169_0_growReduce_InvokeMethod(EOS(STATIC_2169), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, matching2, o885) → f2176_1_growReduce_InvokeMethod(f2176_0_growReduce_Load(EOS(STATIC_2176), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), o533, 1, o885) | &&(=(matching1, 0), =(matching2, 1))
f2172_0_growReduce_Load(EOS(STATIC_2172), i312, java.lang.Object(o878sub), o533, java.lang.Object(o878sub), i314) → f2178_0_growReduce_InvokeMethod(EOS(STATIC_2178), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2173_0__init__Load(EOS(STATIC_2173), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2179_0__init__FieldAccess(EOS(STATIC_2179), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2175_0_growReduce_Load(EOS(STATIC_2175), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896) → f2183_0_growReduce_ConstantStackPush(EOS(STATIC_2183), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315)
f2176_0_growReduce_Load(EOS(STATIC_2176), matching1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), matching2, o885) → f2185_0_growReduce_Load(EOS(STATIC_2185), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885) | &&(=(matching1, 1), =(matching2, 1))
f2178_0_growReduce_InvokeMethod(EOS(STATIC_2178), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2186_1_growReduce_InvokeMethod(f2186_0_growReduce_Load(EOS(STATIC_2186), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)), i312, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2179_0__init__FieldAccess(EOS(STATIC_2179), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), java.lang.Object(o878sub)) → f2190_0__init__Return(EOS(STATIC_2190), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(o878sub)) | &&(=(matching1, 1), =(matching2, 1))
f2183_0_growReduce_ConstantStackPush(EOS(STATIC_2183), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315) → f2193_0_growReduce_LE(EOS(STATIC_2193), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315, 2)
f2185_0_growReduce_Load(EOS(STATIC_2185), matching1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), matching2, o885) → f2198_0_growReduce_Load(EOS(STATIC_2198), 1, o885, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o885)), 1, o885) | &&(=(matching1, 1), =(matching2, 1))
f2186_0_growReduce_Load(EOS(STATIC_2186), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2200_0_growReduce_Load(EOS(STATIC_2200), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2190_0__init__Return(EOS(STATIC_2190), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), java.lang.Object(o878sub)) → f2201_0_growReduce_Store(EOS(STATIC_2201), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2193_0_growReduce_LE(EOS(STATIC_2193), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, i315, o896, i315, matching1) → f2203_0_growReduce_ConstantStackPush(EOS(STATIC_2203), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896) | &&(>(i315, 2), =(matching1, 2))
f2198_0_growReduce_Load(EOS(STATIC_2198), matching1, o911, o912, o914, matching2, o911) → f2208_0_growReduce_Load(EOS(STATIC_2208), 1, o911, o912, 1, o911) | &&(=(matching1, 1), =(matching2, 1))
f2201_0_growReduce_Store(EOS(STATIC_2201), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2210_0_growReduce_JMP(EOS(STATIC_2210), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2203_0_growReduce_ConstantStackPush(EOS(STATIC_2203), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896) → f2211_0_growReduce_Load(EOS(STATIC_2211), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896, 0)
f2210_0_growReduce_JMP(EOS(STATIC_2210), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2233_0_growReduce_Inc(EOS(STATIC_2233), 1, java.lang.Object(o878sub), o533, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2211_0_growReduce_Load(EOS(STATIC_2211), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, o896, matching1) → f2235_0_growReduce_InvokeMethod(EOS(STATIC_2235), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, 0, o896) | =(matching1, 0)
f2233_0_growReduce_Inc(EOS(STATIC_2233), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2240_0_growReduce_Load(EOS(STATIC_2240), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 1))
f2235_0_growReduce_InvokeMethod(EOS(STATIC_2235), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, matching1, o896) → f2242_1_growReduce_InvokeMethod(f2242_0_growReduce_Load(EOS(STATIC_2242), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), o533, 0, o896) | =(matching1, 0)
f2236_0_growReduce_Return(EOS(STATIC_2236), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o930, matching2, NULL, i320, NULL) → f2244_0_growReduce_Return(EOS(STATIC_2244), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o930) | &&(=(matching1, 0), =(matching2, 1))
f2240_0_growReduce_Load(EOS(STATIC_2240), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2248_0_growReduce_ConstantStackPush(EOS(STATIC_2248), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2) | &&(=(matching1, 1), =(matching2, 2))
f2242_0_growReduce_Load(EOS(STATIC_2242), matching1, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), matching2, o896) → f2250_0_growReduce_Load(EOS(STATIC_2250), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896) | &&(=(matching1, 0), =(matching2, 0))
f2248_0_growReduce_ConstantStackPush(EOS(STATIC_2248), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching3) → f2254_0_growReduce_LE(EOS(STATIC_2254), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2, 2) | &&(&&(=(matching1, 1), =(matching2, 2)), =(matching3, 2))
f2250_0_growReduce_Load(EOS(STATIC_2250), matching1, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), matching2, o896) → f2260_0_growReduce_Load(EOS(STATIC_2260), 0, o896, o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o896)), 0, o896) | &&(=(matching1, 0), =(matching2, 0))
f2254_0_growReduce_LE(EOS(STATIC_2254), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching3, matching4) → f2285_0_growReduce_Load(EOS(STATIC_2285), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(&&(&&(=(matching1, 1), =(matching2, 2)), =(matching3, 2)), =(matching4, 2))
f2260_0_growReduce_Load(EOS(STATIC_2260), matching1, o965, o966, o968, matching2, o965) → f2289_0_growReduce_Load(EOS(STATIC_2289), 0, o965, o966, 0, o965) | &&(=(matching1, 0), =(matching2, 0))
f2285_0_growReduce_Load(EOS(STATIC_2285), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2294_0_growReduce_Load(EOS(STATIC_2294), 1, java.lang.Object(o878sub), o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), 2) | &&(=(matching1, 1), =(matching2, 2))
f2291_0_growReduce_Return(EOS(STATIC_2291), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o983, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2629_0_growReduce_Return(EOS(STATIC_2629), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o983, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 0), =(matching2, 1))
f2292_0_growReduce_Return(EOS(STATIC_2292), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1000, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2427_0_growReduce_Return(EOS(STATIC_2427), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1000, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
f2294_0_growReduce_Load(EOS(STATIC_2294), matching1, java.lang.Object(o878sub), o533, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), matching2) → f2323_0_growReduce_InvokeMethod(EOS(STATIC_2323), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 2))
f2323_0_growReduce_InvokeMethod(EOS(STATIC_2323), matching1, java.lang.Object(o878sub), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2330_1_growReduce_InvokeMethod(f2330_0_growReduce_Load(EOS(STATIC_2330), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))), 1, java.lang.Object(o878sub), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 1), =(matching2, 2))
f2324_0_growReduce_Return(EOS(STATIC_2324), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025, matching1, NULL, matching2, NULL) → f2332_0_growReduce_JMP(EOS(STATIC_2332), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025) | &&(=(matching1, 0), =(matching2, 0))
f2325_0_growReduce_Return(EOS(STATIC_2325), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1038, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2650_0_growReduce_Return(EOS(STATIC_2650), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1038, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | =(matching1, 0)
f2330_0_growReduce_Load(EOS(STATIC_2330), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2404_0_growReduce_Load(EOS(STATIC_2404), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 2), =(matching2, 2))
f2332_0_growReduce_JMP(EOS(STATIC_2332), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025) → f2408_0_growReduce_Return(EOS(STATIC_2408), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025)
f2404_0_growReduce_Load(EOS(STATIC_2404), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, java.lang.Object(o878sub), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) → f2465_0_growReduce_Load(EOS(STATIC_2465), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub))), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o878sub)))) | &&(=(matching1, 2), =(matching2, 2))
f2427_0_growReduce_Return(EOS(STATIC_2427), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1183)), o1184, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1183))) → f2450_0_growReduce_Return(EOS(STATIC_2450), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1183)), o1184, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1183))) | =(matching1, 0)
f2450_0_growReduce_Return(EOS(STATIC_2450), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1201)), o1202, i404, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1201))) → f2462_0_growReduce_Return(EOS(STATIC_2462), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1201)), o1202)
f2607_0_growReduce_Return(EOS(STATIC_2607), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1247, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2291_0_growReduce_Return(EOS(STATIC_2291), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1247, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 0), =(matching2, 1))
f2629_0_growReduce_Return(EOS(STATIC_2629), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1519)))), o1520, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1519))) → f3099_0_growReduce_Return(EOS(STATIC_3099), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1519)))), o1520, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1519))) | &&(=(matching1, 0), =(matching2, 1))
f2650_0_growReduce_Return(EOS(STATIC_2650), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546))) → f2698_0_growReduce_JMP(EOS(STATIC_2698), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547) | =(matching1, 0)
f2698_0_growReduce_JMP(EOS(STATIC_2698), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547) → f2723_0_growReduce_Return(EOS(STATIC_2723), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547)
f2703_0_growReduce_Return(EOS(STATIC_2703), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573)))), o1578, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573))) → f2629_0_growReduce_Return(EOS(STATIC_2629), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573)))), o1578, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573))) | &&(=(matching1, 0), =(matching2, 1))
f2710_0_growReduce_Return(EOS(STATIC_2710), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)), o1593, i534, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589))) → f2450_0_growReduce_Return(EOS(STATIC_2450), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)), o1593, i534, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)))
f2723_0_growReduce_Return(EOS(STATIC_2723), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547) → f2875_0_growReduce_Return(EOS(STATIC_2875), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1546)))), o1547)
f2892_0_growReduce_Return(EOS(STATIC_2892), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879)), o1884, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879))))) → f2893_0_growReduce_Return(EOS(STATIC_2893), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879)), o1884, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879))))) | &&(=(matching1, 1), =(matching2, 2))
f2893_0_growReduce_Return(EOS(STATIC_2893), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1900)), o1901, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1900))))) → f3038_0_growReduce_Return(EOS(STATIC_3038), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1900)), o1901, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1900))))) | &&(=(matching1, 1), =(matching2, 2))
f3021_0_growReduce_Return(EOS(STATIC_3021), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub))))), o2035, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub)))) → f2629_0_growReduce_Return(EOS(STATIC_2629), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub))))), o2035, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub)))) | &&(=(matching1, 0), =(matching2, 1))
f3037_0_growReduce_Return(EOS(STATIC_3037), matching1, java.lang.Object(o2085sub), o2080, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2085sub)))) → f3038_0_growReduce_Return(EOS(STATIC_3038), 1, java.lang.Object(o2085sub), o2080, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2085sub)))) | &&(=(matching1, 1), =(matching2, 2))
f3038_0_growReduce_Return(EOS(STATIC_3038), matching1, java.lang.Object(o2095sub), o2096, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2095sub)))) → f3044_0_growReduce_Return(EOS(STATIC_3044), 1, java.lang.Object(o2095sub), o2096) | &&(=(matching1, 1), =(matching2, 2))
f3098_0_growReduce_Return(EOS(STATIC_3098), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2144sub))), o2138, matching2, java.lang.Object(o2144sub)) → f3099_0_growReduce_Return(EOS(STATIC_3099), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2144sub))), o2138, 1, java.lang.Object(o2144sub)) | &&(=(matching1, 0), =(matching2, 1))
f3099_0_growReduce_Return(EOS(STATIC_3099), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2189sub))), o2190, matching2, java.lang.Object(o2189sub)) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2189sub))), o2190) | &&(=(matching1, 0), =(matching2, 1))
f3197_0_growReduce_Return(EOS(STATIC_3197), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub))))), o2238, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub)))) → f3099_0_growReduce_Return(EOS(STATIC_3099), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub))))), o2238, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub)))) | &&(=(matching1, 0), =(matching2, 1))
f3208_0_growReduce_Return(EOS(STATIC_3208), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub))), o2256, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub)))) → f2450_0_growReduce_Return(EOS(STATIC_2450), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub))), o2256, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub)))) | =(matching1, 0)
f3218_0_growReduce_Return(EOS(STATIC_3218), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub))))), o2271, matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub)))) → f2650_0_growReduce_Return(EOS(STATIC_2650), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub))))), o2271, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub)))) | =(matching1, 0)
f2208_0_growReduce_Load(EOS(STATIC_2208), matching1, o911, o912, matching2, o911) → f2075_0_growReduce_Load(EOS(STATIC_2075), 1, o911, o912, 1, o911) | &&(=(matching1, 1), =(matching2, 1))
f2200_0_growReduce_Load(EOS(STATIC_2200), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub)) → f2075_0_growReduce_Load(EOS(STATIC_2075), i314, java.lang.Object(o878sub), o533, i314, java.lang.Object(o878sub))
f2289_0_growReduce_Load(EOS(STATIC_2289), matching1, o965, o966, matching2, o965) → f2075_0_growReduce_Load(EOS(STATIC_2075), 0, o965, o966, 0, o965) | &&(=(matching1, 0), =(matching2, 0))
f2465_0_growReduce_Load(EOS(STATIC_2465), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533)), o533, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533))) → f2075_0_growReduce_Load(EOS(STATIC_2075), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533)), o533, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o533))) | &&(=(matching1, 2), =(matching2, 2))
f2176_1_growReduce_InvokeMethod(f2085_0_growReduce_Return(EOS(STATIC_2085), i320, NULL, o930, i320, NULL), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o930, matching2, NULL) → f2236_0_growReduce_Return(EOS(STATIC_2236), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o930, 1, NULL, i320, NULL) | &&(=(matching1, 0), =(matching2, 1))
f2176_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o983), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o983, matching3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2291_0_growReduce_Return(EOS(STATIC_2291), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o983, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f2176_1_growReduce_InvokeMethod(f2408_0_growReduce_Return(EOS(STATIC_2408), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1247), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1247, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2607_0_growReduce_Return(EOS(STATIC_2607), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1247, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 0), =(matching2, 1))
f2176_1_growReduce_InvokeMethod(f2462_0_growReduce_Return(EOS(STATIC_2462), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573)), o1578), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573)))), o1578, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573))) → f2703_0_growReduce_Return(EOS(STATIC_2703), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573)))), o1578, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1573))) | &&(=(matching1, 0), =(matching2, 1))
f2176_1_growReduce_InvokeMethod(f2875_0_growReduce_Return(EOS(STATIC_2875), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub))), o2035), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub))))), o2035, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub)))) → f3021_0_growReduce_Return(EOS(STATIC_3021), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub))))), o2035, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2030sub)))) | &&(=(matching1, 0), =(matching2, 1))
f2176_1_growReduce_InvokeMethod(f3044_0_growReduce_Return(EOS(STATIC_3044), matching1, java.lang.Object(o2144sub), o2138), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2144sub))), o2138, matching3, java.lang.Object(o2144sub)) → f3098_0_growReduce_Return(EOS(STATIC_3098), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2144sub))), o2138, 1, java.lang.Object(o2144sub)) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
f2176_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub))), o2238), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub))))), o2238, matching3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub)))) → f3197_0_growReduce_Return(EOS(STATIC_3197), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub))))), o2238, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2233sub)))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
f2186_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1000), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1000, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2292_0_growReduce_Return(EOS(STATIC_2292), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1000, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 0), =(matching2, 0))
f2186_1_growReduce_InvokeMethod(f2462_0_growReduce_Return(EOS(STATIC_2462), i534, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)), o1593), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)), o1593, i534, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589))) → f2710_0_growReduce_Return(EOS(STATIC_2710), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)), o1593, i534, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1589)))
f2186_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub))), o2256), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub))), o2256, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub)))) → f3208_0_growReduce_Return(EOS(STATIC_3208), i312, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub))), o2256, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2252sub)))) | &&(=(matching1, 0), =(matching2, 0))
f2242_1_growReduce_InvokeMethod(f2085_0_growReduce_Return(EOS(STATIC_2085), matching1, NULL, o1025, matching2, NULL), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025, matching3, NULL) → f2324_0_growReduce_Return(EOS(STATIC_2324), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1025, 0, NULL, 0, NULL) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
f2242_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), o1038), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1038, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2325_0_growReduce_Return(EOS(STATIC_2325), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), o1038, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) | &&(=(matching1, 0), =(matching2, 0))
f2242_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub))), o2271), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub))))), o2271, matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub)))) → f3218_0_growReduce_Return(EOS(STATIC_3218), i313, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub))))), o2271, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2265sub)))) | &&(=(matching1, 0), =(matching2, 0))
f2330_1_growReduce_InvokeMethod(f2723_0_growReduce_Return(EOS(STATIC_2723), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879)))), o1884), matching2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879)), o1884, matching3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879))))) → f2892_0_growReduce_Return(EOS(STATIC_2892), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879)), o1884, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, o1879))))) | &&(&&(=(matching1, 2), =(matching2, 1)), =(matching3, 2))
f2330_1_growReduce_InvokeMethod(f2875_0_growReduce_Return(EOS(STATIC_2875), matching1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2085sub))), o2080), matching2, java.lang.Object(o2085sub), o2080, matching3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2085sub)))) → f3037_0_growReduce_Return(EOS(STATIC_3037), 1, java.lang.Object(o2085sub), o2080, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(o2085sub)))) | &&(&&(=(matching1, 2), =(matching2, 1)), =(matching3, 2))

Combined rules. Obtained 4 conditional rules for P and 20 conditional rules for R.


P rules:
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), x0, java.lang.Object(x1), x2, x0, java.lang.Object(x1), java.lang.Object(x1)) → f2186_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), +(x0, 1), java.lang.Object(x1), x2, +(x0, 1), java.lang.Object(x1), java.lang.Object(x1)), x0, java.lang.Object(x1), x2, +(x0, 1), java.lang.Object(x1)) | &&(<(x0, 1), <(x0, 0))
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 1, java.lang.Object(x1), java.lang.Object(x1), 1, java.lang.Object(x1), java.lang.Object(x1)) → f2330_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))), 1, java.lang.Object(x1), java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f2242_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 0, x1, x2, 0, x1, x1), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 0, x1) | >(x0, 1)
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f2176_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 1, x1, x2, 1, x1, x1), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 1, x1)
R rules:
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), x0, NULL, x1, x0, NULL, NULL) → f2085_0_growReduce_Return(EOS(STATIC_2085), x0, NULL, x1, x0, NULL)
f2176_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1)
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), x0, java.lang.Object(x1), x2, x0, java.lang.Object(x1), java.lang.Object(x1)) → f2186_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), +(x0, 1), java.lang.Object(x1), x2, +(x0, 1), java.lang.Object(x1), java.lang.Object(x1)), x0, java.lang.Object(x1), x2, +(x0, 1), java.lang.Object(x1)) | &&(<(x0, 1), <(x0, 0))
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f2176_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 1, x1, x2, 1, x1, x1), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 1, x1)
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f2242_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 0, x1, x2, 0, x1, x1), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 0, x1) | >(x0, 1)
f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 1, java.lang.Object(x1), java.lang.Object(x1), 1, java.lang.Object(x1), java.lang.Object(x1)) → f2330_1_growReduce_InvokeMethod(f2078_0_growReduce_NONNULL(EOS(STATIC_2078), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))), 1, java.lang.Object(x1), java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))
f2176_1_growReduce_InvokeMethod(f2085_0_growReduce_Return(EOS(STATIC_2085), x0, NULL, x1, x0, NULL), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1, 1, NULL) → f2244_0_growReduce_Return(EOS(STATIC_2244), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1)
f2176_1_growReduce_InvokeMethod(f2408_0_growReduce_Return(EOS(STATIC_2408), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1)
f2176_1_growReduce_InvokeMethod(f2462_0_growReduce_Return(EOS(STATIC_2462), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)))), x2, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)))), x2)
f2176_1_growReduce_InvokeMethod(f2875_0_growReduce_Return(EOS(STATIC_2875), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2)
f2176_1_growReduce_InvokeMethod(f3044_0_growReduce_Return(EOS(STATIC_3044), 1, java.lang.Object(x1), x2), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2, 1, java.lang.Object(x1)) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2)
f2176_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2, 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))) → f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2)
f2186_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1), x2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2462_0_growReduce_Return(EOS(STATIC_2462), x2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1)
f2186_1_growReduce_InvokeMethod(f2462_0_growReduce_Return(EOS(STATIC_2462), x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))) → f2462_0_growReduce_Return(EOS(STATIC_2462), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2)
f2186_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))) → f2462_0_growReduce_Return(EOS(STATIC_2462), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2)
f2242_1_growReduce_InvokeMethod(f2085_0_growReduce_Return(EOS(STATIC_2085), 0, NULL, x1, 0, NULL), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1, 0, NULL) → f2408_0_growReduce_Return(EOS(STATIC_2408), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1)
f2242_1_growReduce_InvokeMethod(f2244_0_growReduce_Return(EOS(STATIC_2244), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)), x1), x2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL))) → f2875_0_growReduce_Return(EOS(STATIC_2875), x2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, NULL)))), x1)
f2242_1_growReduce_InvokeMethod(f3114_0_growReduce_Return(EOS(STATIC_3114), 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))) → f2875_0_growReduce_Return(EOS(STATIC_2875), x3, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))))), x2)
f2330_1_growReduce_InvokeMethod(f2723_0_growReduce_Return(EOS(STATIC_2723), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)))), x2), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1))))) → f3044_0_growReduce_Return(EOS(STATIC_3044), 1, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, x1)), x2)
f2330_1_growReduce_InvokeMethod(f2875_0_growReduce_Return(EOS(STATIC_2875), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1))), x2), 1, java.lang.Object(x1), x2, 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(EOC, java.lang.Object(x1)))) → f3044_0_growReduce_Return(EOS(STATIC_3044), 1, java.lang.Object(x1), x2)

Filtered ground terms:



f2078_0_growReduce_NONNULL(x1, x2, x3, x4, x5, x6, x7) → f2078_0_growReduce_NONNULL(x2, x3, x4, x5, x6, x7)
Cond_f2078_0_growReduce_NONNULL(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2078_0_growReduce_NONNULL(x1, x3, x4, x5, x6, x7, x8)
f2330_1_growReduce_InvokeMethod(x1, x2, x3, x4, x5, x6) → f2330_1_growReduce_InvokeMethod(x1, x3, x4, x6)
Cond_f2078_0_growReduce_NONNULL1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2078_0_growReduce_NONNULL1(x1, x3, x4, x5, x6, x7, x8)
f2242_1_growReduce_InvokeMethod(x1, x2, x3, x4, x5, x6) → f2242_1_growReduce_InvokeMethod(x1, x2, x3, x4, x6)
f2176_1_growReduce_InvokeMethod(x1, x2, x3, x4, x5, x6) → f2176_1_growReduce_InvokeMethod(x1, x3, x4, x6)
AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1, x2) → AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)
f2085_0_growReduce_Return(x1, x2, x3, x4, x5, x6) → f2085_0_growReduce_Return(x2, x4, x5)
f3114_0_growReduce_Return(x1, x2, x3, x4) → f3114_0_growReduce_Return(x3, x4)
f2244_0_growReduce_Return(x1, x2, x3, x4) → f2244_0_growReduce_Return(x4)
f2462_0_growReduce_Return(x1, x2, x3, x4) → f2462_0_growReduce_Return(x2, x3, x4)
f2408_0_growReduce_Return(x1, x2, x3, x4) → f2408_0_growReduce_Return(x2, x4)
f2875_0_growReduce_Return(x1, x2, x3, x4) → f2875_0_growReduce_Return(x2, x3, x4)
f3044_0_growReduce_Return(x1, x2, x3, x4) → f3044_0_growReduce_Return(x3, x4)
f2723_0_growReduce_Return(x1, x2, x3, x4) → f2723_0_growReduce_Return(x3, x4)

Filtered unneeded arguments:



f2186_1_growReduce_InvokeMethod(x1, x2, x3, x4, x5, x6) → f2186_1_growReduce_InvokeMethod(x1, x3, x5, x6)
f2330_1_growReduce_InvokeMethod(x1, x2, x3, x4) → f2330_1_growReduce_InvokeMethod(x1, x2, x4)
f2242_1_growReduce_InvokeMethod(x1, x2, x3, x4, x5) → f2242_1_growReduce_InvokeMethod(x1, x2, x3, x5)
f2176_1_growReduce_InvokeMethod(x1, x2, x3, x4) → f2176_1_growReduce_InvokeMethod(x1, x2, x4)
f2085_0_growReduce_Return(x1, x2, x3) → f2085_0_growReduce_Return(x1, x3)
f2462_0_growReduce_Return(x1, x2, x3) → f2462_0_growReduce_Return(x2)
f2875_0_growReduce_Return(x1, x2, x3) → f2875_0_growReduce_Return(x1, x2)
f3044_0_growReduce_Return(x1, x2) → f3044_0_growReduce_Return(x1)
f3114_0_growReduce_Return(x1, x2) → f3114_0_growReduce_Return(x1)
f2723_0_growReduce_Return(x1, x2) → f2723_0_growReduce_Return(x1)

Filtered duplicate args:



f2078_0_growReduce_NONNULL(x1, x2, x3, x4, x5, x6) → f2078_0_growReduce_NONNULL(x3, x4, x6)
Cond_f2078_0_growReduce_NONNULL(x1, x2, x3, x4, x5, x6, x7) → Cond_f2078_0_growReduce_NONNULL(x1, x4, x5, x7)
f2186_1_growReduce_InvokeMethod(x1, x2, x3, x4) → f2186_1_growReduce_InvokeMethod(x1, x3, x4)
f2330_1_growReduce_InvokeMethod(x1, x2, x3) → f2330_1_growReduce_InvokeMethod(x1, x3)
Cond_f2078_0_growReduce_NONNULL1(x1, x2, x3, x4, x5, x6, x7) → Cond_f2078_0_growReduce_NONNULL1(x1, x4, x5, x7)
f2242_1_growReduce_InvokeMethod(x1, x2, x3, x4) → f2242_1_growReduce_InvokeMethod(x1, x2, x3)
f2176_1_growReduce_InvokeMethod(x1, x2, x3) → f2176_1_growReduce_InvokeMethod(x1, x2)
f2085_0_growReduce_Return(x1, x2) → f2085_0_growReduce_Return(x2)

Combined rules. Obtained 4 conditional rules for P and 0 conditional rules for R.


P rules:
F2078_0_GROWREDUCE_NONNULL(x2, x0, java.lang.Object(x1)) → F2078_0_GROWREDUCE_NONNULL(x2, +(x0, 1), java.lang.Object(x1)) | &&(<(x0, 0), <(x0, 1))
F2078_0_GROWREDUCE_NONNULL(java.lang.Object(x1), 1, java.lang.Object(x1)) → F2078_0_GROWREDUCE_NONNULL(java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
F2078_0_GROWREDUCE_NONNULL(x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL(x2, 0, x1) | >(x0, 1)
F2078_0_GROWREDUCE_NONNULL(x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL(x2, 1, x1)
R rules:

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


P rules:
F2078_0_GROWREDUCE_NONNULL'(x2, x0, java.lang.Object(x1)) → COND_F2078_0_GROWREDUCE_NONNULL(&&(<(x0, 0), <(x0, 1)), x2, x0, java.lang.Object(x1))
COND_F2078_0_GROWREDUCE_NONNULL(TRUE, x2, x0, java.lang.Object(x1)) → F2078_0_GROWREDUCE_NONNULL'(x2, +(x0, 1), java.lang.Object(x1))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1), 1, java.lang.Object(x1)) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1))))
F2078_0_GROWREDUCE_NONNULL'(x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → COND_F2078_0_GROWREDUCE_NONNULL1(>(x0, 1), x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)))
COND_F2078_0_GROWREDUCE_NONNULL1(TRUE, x2, x0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL'(x2, 0, x1)
F2078_0_GROWREDUCE_NONNULL'(x2, 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL'(x2, 1, x1)
R rules:

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

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(x0[0] < 0 && x0[0] < 1, x2[0], x0[0], java.lang.Object(x1[0]))
(1): COND_F2078_0_GROWREDUCE_NONNULL(TRUE, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], x0[1] + 1, java.lang.Object(x1[1]))
(2): F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), 1, java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), 2, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
(3): F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(x0[3] > 1, x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
(4): COND_F2078_0_GROWREDUCE_NONNULL1(TRUE, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], 0, x1[4])
(5): F2078_0_GROWREDUCE_NONNULL'(x2[5], 0, java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], 1, x1[5])

(0) -> (1), if (x0[0] < 0 && x0[0] < 1 ∧x2[0] →* x2[1]∧x0[0] →* x0[1]∧java.lang.Object(x1[0]) →* java.lang.Object(x1[1]))


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


(1) -> (2), if (x2[1] →* java.lang.Object(x1[2])∧x0[1] + 1 →* 1∧java.lang.Object(x1[1]) →* java.lang.Object(x1[2]))


(1) -> (3), if (x2[1] →* x2[3]∧x0[1] + 1 →* x0[3]∧java.lang.Object(x1[1]) →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))


(1) -> (5), if (x2[1] →* x2[5]∧x0[1] + 1 →* 0∧java.lang.Object(x1[1]) →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5])))


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


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


(2) -> (3), if (java.lang.Object(x1[2]) →* x2[3]∧2 →* x0[3]∧java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))) →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))


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


(3) -> (4), if (x0[3] > 1 ∧x2[3] →* x2[4]∧x0[3] →* x0[4]∧java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])) →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4])))


(4) -> (0), if (x2[4] →* x2[0]∧0 →* x0[0]∧x1[4] →* java.lang.Object(x1[0]))


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


(4) -> (3), if (x2[4] →* x2[3]∧0 →* x0[3]∧x1[4] →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))


(4) -> (5), if (x2[4] →* x2[5]∧x1[4] →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5])))


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


(5) -> (2), if (x2[5] →* java.lang.Object(x1[2])∧x1[5] →* java.lang.Object(x1[2]))


(5) -> (3), if (x2[5] →* x2[3]∧1 →* x0[3]∧x1[5] →* java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))


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



The set Q is empty.

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
less_int(pos(01), pos(01)) → false
less_int(pos(01), neg(01)) → false
less_int(neg(01), pos(01)) → false
less_int(neg(01), neg(01)) → false
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(pos(01), neg(s(y))) → false
less_int(neg(01), neg(s(y))) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(s(x)), neg(01)) → false
less_int(neg(s(x)), neg(01)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greater_int(pos(01), pos(01)) → false
greater_int(pos(01), neg(01)) → false
greater_int(neg(01), pos(01)) → false
greater_int(neg(01), neg(01)) → false
greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(pos(01), neg(s(y))) → true
greater_int(neg(01), neg(s(y))) → true
greater_int(pos(s(x)), pos(01)) → true
greater_int(neg(s(x)), pos(01)) → false
greater_int(pos(s(x)), neg(01)) → true
greater_int(neg(s(x)), neg(01)) → false
greater_int(pos(s(x)), neg(s(y))) → true
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(neg(s(x)), neg(s(y))) → greater_int(neg(x), neg(y))

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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:

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(12) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

and(false, true) → false

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 0   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = x1 + x4   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 2·x4   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 2   
POL(and(x1, x2)) = x2   
POL(false) = 0   
POL(greater_int(x1, x2)) = 2   
POL(java.lang.Object(x1)) = 1   
POL(less_int(x1, x2)) = x2   
POL(minus_nat(x1, x2)) = 1   
POL(neg(x1)) = 0   
POL(plus_int(x1, x2)) = x1   
POL(plus_nat(x1, x2)) = 2 + x1 + x2   
POL(pos(x1)) = 1   
POL(s(x1)) = 0   
POL(true) = 1   

(13) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, 01) → pos(01)
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), 01) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(14) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

minus_nat(01, 01) → pos(01)
minus_nat(s(x), 01) → pos(s(x))

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 1   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = 2·x2 + 2·x3   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 2·x2 + x3   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 2·x1 + 2·x2   
POL(and(x1, x2)) = 2 + 2·x1 + x2   
POL(false) = 0   
POL(greater_int(x1, x2)) = 2·x2   
POL(java.lang.Object(x1)) = 1   
POL(less_int(x1, x2)) = 0   
POL(minus_nat(x1, x2)) = 1   
POL(neg(x1)) = 1 + x1   
POL(plus_int(x1, x2)) = x1 + x2   
POL(plus_nat(x1, x2)) = 2 + x2   
POL(pos(x1)) = 0   
POL(s(x1)) = 0   
POL(true) = 0   

(15) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(neg(01), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(16) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

greater_int(neg(01), pos(s(y))) → false
greater_int(neg(s(x)), pos(s(y))) → false

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 2   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = 2·x3 + 2·x4   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = x1   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 2·x2   
POL(and(x1, x2)) = 0   
POL(false) = 0   
POL(greater_int(x1, x2)) = x1   
POL(java.lang.Object(x1)) = 0   
POL(less_int(x1, x2)) = x1   
POL(minus_nat(x1, x2)) = 1   
POL(neg(x1)) = 1   
POL(plus_int(x1, x2)) = x2   
POL(plus_nat(x1, x2)) = x2   
POL(pos(x1)) = 0   
POL(s(x1)) = 0   
POL(true) = 0   

(17) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(18) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

minus_nat(s(x), s(y)) → minus_nat(x, y)

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 0   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = x3   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 0   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = x2   
POL(and(x1, x2)) = 0   
POL(false) = 0   
POL(greater_int(x1, x2)) = 0   
POL(java.lang.Object(x1)) = 0   
POL(less_int(x1, x2)) = 1   
POL(minus_nat(x1, x2)) = 2·x2   
POL(neg(x1)) = 2·x1   
POL(plus_int(x1, x2)) = x2   
POL(plus_nat(x1, x2)) = 2·x1 + 2·x2   
POL(pos(x1)) = 0   
POL(s(x1)) = 2 + x1   
POL(true) = 0   

(19) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(01), pos(01)) → false
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(20) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

greater_int(pos(01), pos(01)) → false

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 1   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 2·x1   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = 1   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = x1   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 1   
POL(and(x1, x2)) = 2   
POL(false) = 0   
POL(greater_int(x1, x2)) = x2   
POL(java.lang.Object(x1)) = 2·x1   
POL(less_int(x1, x2)) = 1   
POL(minus_nat(x1, x2)) = 0   
POL(neg(x1)) = 0   
POL(plus_int(x1, x2)) = x2   
POL(plus_nat(x1, x2)) = x2   
POL(pos(x1)) = x1   
POL(s(x1)) = x1   
POL(true) = 1   

(21) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(01), pos(s(y))) → false
greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(22) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

greater_int(pos(01), pos(s(y))) → false

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 2 + x1   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = x2 + 2·x3   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 2·x1 + x2   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = x1 + 2·x2   
POL(and(x1, x2)) = 2·x1   
POL(false) = 0   
POL(greater_int(x1, x2)) = x1   
POL(java.lang.Object(x1)) = 0   
POL(less_int(x1, x2)) = 2·x1   
POL(minus_nat(x1, x2)) = 2   
POL(neg(x1)) = 2   
POL(plus_int(x1, x2)) = x2   
POL(plus_nat(x1, x2)) = 2 + 2·x2   
POL(pos(x1)) = 1   
POL(s(x1)) = 0   
POL(true) = 1   

(23) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(false, false) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(24) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

and(false, false) → false
and(true, false) → false

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 0   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 0   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = x1 + x2   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 1 + x2   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 1 + x1   
POL(and(x1, x2)) = 1   
POL(false) = 0   
POL(greater_int(x1, x2)) = 1   
POL(java.lang.Object(x1)) = 2·x1   
POL(less_int(x1, x2)) = 2   
POL(minus_nat(x1, x2)) = 0   
POL(neg(x1)) = 0   
POL(plus_int(x1, x2)) = 2   
POL(plus_nat(x1, x2)) = 1 + x2   
POL(pos(x1)) = 0   
POL(s(x1)) = 0   
POL(true) = 1   

(25) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(neg(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(26) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.

Strictly oriented rules of the TRS R:

less_int(neg(01), pos(01)) → false
less_int(neg(01), pos(s(y))) → true

Used ordering: Polynomial interpretation [POLO]:

POL(01) = 1   
POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) = 0   
POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = x1   
POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 0   
POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 2·x2   
POL(and(x1, x2)) = x1 + x2   
POL(false) = 0   
POL(greater_int(x1, x2)) = 1   
POL(java.lang.Object(x1)) = 2·x1   
POL(less_int(x1, x2)) = x1   
POL(minus_nat(x1, x2)) = 0   
POL(neg(x1)) = x1   
POL(plus_int(x1, x2)) = 0   
POL(plus_nat(x1, x2)) = x2   
POL(pos(x1)) = 0   
POL(s(x1)) = 0   
POL(true) = 0   

(27) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


COND_F2078_0_GROWREDUCE_NONNULL(true, x2[1], x0[1], java.lang.Object(x1[1])) → F2078_0_GROWREDUCE_NONNULL'(x2[1], plus_int(pos(s(01)), x0[1]), java.lang.Object(x1[1]))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(F2078_0_GROWREDUCE_NONNULL'(x1, x2, x3)) = 0 +
[0,0]
·x1 +
[1,0]
·x2 +
[0,0]
·x3

POL(java.lang.Object(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(COND_F2078_0_GROWREDUCE_NONNULL(x1, x2, x3, x4)) = 0 +
[0,1]
·x1 +
[0,0]
·x2 +
[0,0]
·x3 +
[0,0]
·x4

POL(and(x1, x2)) =
/0\
\0/
 +
/00\
\01/
·x1 +
/00\
\00/
·x2

POL(less_int(x1, x2)) =
/0\
\0/
 +
/01\
\10/
·x1 +
/00\
\00/
·x2

POL(pos(x1)) =
/0\
\0/
 +
/00\
\10/
·x1

POL(01) =
/1\
\0/

POL(s(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(true) =
/0\
\1/

POL(plus_int(x1, x2)) =
/0\
\0/
 +
/01\
\01/
·x1 +
/00\
\01/
·x2

POL(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(COND_F2078_0_GROWREDUCE_NONNULL1(x1, x2, x3, x4)) = 0 +
[0,0]
·x1 +
[0,0]
·x2 +
[0,0]
·x3 +
[0,0]
·x4

POL(greater_int(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(false) =
/0\
\0/

POL(neg(x1)) =
/1\
\0/
 +
/00\
\11/
·x1

POL(minus_nat(x1, x2)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/00\
\00/
·x2

POL(plus_nat(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/10\
\11/
·x2

The following usable rules [FROCOS05] were oriented:

less_int(pos(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
and(true, true) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

(29) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[0], x0[0], java.lang.Object(x1[0])) → COND_F2078_0_GROWREDUCE_NONNULL(and(less_int(x0[0], pos(01)), less_int(x0[0], pos(s(01)))), x2[0], x0[0], java.lang.Object(x1[0]))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(30) DependencyGraphProof (EQUIVALENT transformation)

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

(31) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(01, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(01, s(y)) → neg(s(y))
less_int(pos(01), pos(01)) → false
less_int(pos(s(x)), pos(01)) → false
less_int(neg(s(x)), pos(01)) → true
less_int(pos(01), pos(s(y))) → true
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
and(true, true) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

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

(33) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))
greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(34) 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].

and(false, false)
and(false, true)
and(true, false)
and(true, true)
less_int(pos(01), pos(01))
less_int(pos(01), neg(01))
less_int(neg(01), pos(01))
less_int(neg(01), neg(01))
less_int(pos(01), pos(s(x0)))
less_int(neg(01), pos(s(x0)))
less_int(pos(01), neg(s(x0)))
less_int(neg(01), neg(s(x0)))
less_int(pos(s(x0)), pos(01))
less_int(neg(s(x0)), pos(01))
less_int(pos(s(x0)), neg(01))
less_int(neg(s(x0)), neg(01))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(01, x0)
plus_nat(s(x0), x1)
minus_nat(01, 01)
minus_nat(01, s(x0))
minus_nat(s(x0), 01)
minus_nat(s(x0), s(x1))

(35) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3])))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(36) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F2078_0_GROWREDUCE_NONNULL'(x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(x0[3], pos(s(01))), x2[3], x0[3], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[3]))) we obtained the following new rules [LPAR04]:

F2078_0_GROWREDUCE_NONNULL'(z0, pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(01), pos(s(01))), z0, pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))
F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(s(01))), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(s(01))), pos(s(01))), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

(37) Obligation:

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

COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(z0, pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(01), pos(s(01))), z0, pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))
F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(s(01))), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(s(01))), pos(s(01))), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(38) DependencyGraphProof (EQUIVALENT transformation)

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

(39) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(s(01))), pos(s(01))), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(s(01))), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(40) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(s(01))), pos(s(01))), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) at position [0] we obtained the following new rules [LPAR04]:

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

(41) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(s(01))), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(42) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(s(01))), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) at position [0] we obtained the following new rules [LPAR04]:

F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(01), pos(01)), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))

(43) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
F2078_0_GROWREDUCE_NONNULL'(z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(01), pos(01)), z0, pos(s(01)), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x2)))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(s(y))) → greater_int(pos(x), pos(y))
greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

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

(47) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(48) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(greater_int(pos(s(01)), pos(01)), java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) at position [0] we obtained the following new rules [LPAR04]:

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

(49) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

The TRS R consists of the following rules:

greater_int(pos(s(x)), pos(01)) → true

The set Q consists of the following terms:

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

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

(51) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

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

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

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

(52) 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].

greater_int(pos(01), pos(01))
greater_int(pos(01), neg(01))
greater_int(neg(01), pos(01))
greater_int(neg(01), neg(01))
greater_int(pos(01), pos(s(x0)))
greater_int(neg(01), pos(s(x0)))
greater_int(pos(01), neg(s(x0)))
greater_int(neg(01), neg(s(x0)))
greater_int(pos(s(x0)), pos(01))
greater_int(neg(s(x0)), pos(01))
greater_int(pos(s(x0)), neg(01))
greater_int(neg(s(x0)), neg(01))
greater_int(pos(s(x0)), neg(s(x1)))
greater_int(neg(s(x0)), pos(s(x1)))
greater_int(pos(s(x0)), pos(s(x1)))
greater_int(neg(s(x0)), neg(s(x1)))

(53) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4])
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))

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

(54) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule COND_F2078_0_GROWREDUCE_NONNULL1(true, x2[4], x0[4], java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[4]))) → F2078_0_GROWREDUCE_NONNULL'(x2[4], pos(01), x1[4]) we obtained the following new rules [LPAR04]:

COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(01), java.lang.Object(z0))

(55) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5])
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(01), java.lang.Object(z0))

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

(56) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1[5]))) → F2078_0_GROWREDUCE_NONNULL'(x2[5], pos(s(01)), x1[5]) we obtained the following new rules [LPAR04]:

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)), pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)), pos(s(01)), x1)

(57) Obligation:

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

F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(01)), java.lang.Object(x1[2])) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(x1[2]), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(x1[2]))))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0))))
COND_F2078_0_GROWREDUCE_NONNULL1(true, java.lang.Object(z0), pos(s(s(01))), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(java.lang.Object(z0)))) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(z0), pos(01), java.lang.Object(z0))
F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)), pos(01), java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1))) → F2078_0_GROWREDUCE_NONNULL'(java.lang.Object(AlternatingGrowReduceRec2.AlternatingGrowReduceRec2(x1)), pos(s(01)), x1)

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

(58) DependencyGraphProof (EQUIVALENT transformation)

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

(59) TRUE

(60) 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:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(61) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f156_0_createList_Duplicate(EOS, i15, i15) → f161_0_createList_ConstantStackPush(EOS, i15, i15)
f161_0_createList_ConstantStackPush(EOS, i15, i15) → f162_0_createList_InvokeMethod(EOS, i15, i15)
f162_0_createList_InvokeMethod(EOS, i15, i15) → f167_0__init__Load(EOS, i15, i15)
f167_0__init__Load(EOS, i15, i15) → f175_0__init__InvokeMethod(EOS, i15, i15)
f175_0__init__InvokeMethod(EOS, i15, i15) → f178_0__init__Load(EOS, i15, i15)
f178_0__init__Load(EOS, i15, i15) → f181_0__init__Load(EOS, i15, i15)
f181_0__init__Load(EOS, i15, i15) → f187_0__init__FieldAccess(EOS, i15, i15)
f187_0__init__FieldAccess(EOS, i15, i15) → f191_0__init__Return(EOS, i15, i15)
f191_0__init__Return(EOS, i15, i15) → f196_0_createList_Store(EOS, i15, i15)
f196_0_createList_Store(EOS, i15, i15) → f201_0_createList_Load(EOS, i15, i15)
f201_0_createList_Load(EOS, i15, i15) → f209_0_createList_ConstantStackPush(EOS, i15, i15, i15)
f209_0_createList_ConstantStackPush(EOS, i15, i15, i15) → f214_0_createList_LE(EOS, i15, i15, i15, 1)
f214_0_createList_LE(EOS, i25, i25, i25, matching1) → f222_0_createList_LE(EOS, i25, i25, i25, 1) | =(matching1, 1)
f222_0_createList_LE(EOS, i25, i25, i25, matching1) → f230_0_createList_Load(EOS, i25, i25) | &&(>(i25, 1), =(matching1, 1))
f230_0_createList_Load(EOS, i25, i25) → f236_0_createList_Load(EOS, i25, i25)
f236_0_createList_Load(EOS, i25, i25) → f241_0_createList_ConstantStackPush(EOS, i25, i25)
f241_0_createList_ConstantStackPush(EOS, i25, i25) → f282_0_createList_IntArithmetic(EOS, i25, i25, 1)
f282_0_createList_IntArithmetic(EOS, i25, i25, matching1) → f285_0_createList_InvokeMethod(EOS, i25, -(i25, 1)) | &&(>(i25, 0), =(matching1, 1))
f285_0_createList_InvokeMethod(EOS, i25, i34) → f288_0_createList_New(EOS, i34, i34)
f285_0_createList_InvokeMethod(EOS, i25, i34) → f288_1_createList_New(EOS, i25, i34, i34)
f288_0_createList_New(EOS, i34, i34) → f293_0_createList_New(EOS, i34, i34)
f293_0_createList_New(EOS, i34, i34) → f153_0_createList_New(EOS, i34, i34)
f153_0_createList_New(EOS, i15, i15) → f156_0_createList_Duplicate(EOS, i15, i15)

Combined rules. Obtained 2 IRules

P rules:
f156_0_createList_Duplicate(EOS, x0, x0) → f288_1_createList_New(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 1)
f156_0_createList_Duplicate(EOS, x0, x0) → f156_0_createList_Duplicate(EOS, -(x0, 1), -(x0, 1)) | >(x0, 1)

Filtered ground terms:


f156_0_createList_Duplicate(x1, x2, x3) → f156_0_createList_Duplicate(x2, x3)
Cond_f156_0_createList_Duplicate(x1, x2, x3, x4) → Cond_f156_0_createList_Duplicate(x1, x3, x4)
f288_1_createList_New(x1, x2, x3, x4) → f288_1_createList_New(x2, x3, x4)
Cond_f156_0_createList_Duplicate1(x1, x2, x3, x4) → Cond_f156_0_createList_Duplicate1(x1, x3, x4)

Filtered duplicate terms:


f156_0_createList_Duplicate(x1, x2) → f156_0_createList_Duplicate(x2)
Cond_f156_0_createList_Duplicate(x1, x2, x3) → Cond_f156_0_createList_Duplicate(x1, x3)
f288_1_createList_New(x1, x2, x3) → f288_1_createList_New(x3)
Cond_f156_0_createList_Duplicate1(x1, x2, x3) → Cond_f156_0_createList_Duplicate1(x1, x3)

Filtered unneeded terms:


Cond_f156_0_createList_Duplicate(x1, x2) → Cond_f156_0_createList_Duplicate(x1)

Prepared 2 rules for path length conversion:

P rules:
f156_0_createList_Duplicate(x0) → f288_1_createList_New(-(x0, 1)) | >(x0, 1)
f156_0_createList_Duplicate(x0) → f156_0_createList_Duplicate(-(x0, 1)) | >(x0, 1)

Finished conversion. Obtained 1 rules.

P rules:
f156_0_createList_Duplicate(x1) → f156_0_createList_Duplicate(-(x1, 1)) | >(x1, 1)

(62) Obligation:

Rules:
f156_0_createList_Duplicate(x1) → f156_0_createList_Duplicate(-(x1, 1)) | >(x1, 1)

(63) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f156_0_createList_Duplicate(x2)] = x2

Therefore the following rule(s) have been dropped:


f156_0_createList_Duplicate(x0) → f156_0_createList_Duplicate(-(x0, 1)) | >(x0, 1)

(64) YES