Termination proof of /tmp/tmpuWPqoV/ConvertRec.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 3110 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 1283 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 256 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇒, 233 ms)

        ↳13 IDP

        ↳14 IDependencyGraphProof (⇔, 0 ms)

        ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIntTRSProof (⇒, 319 ms)

        ↳18 intTRS

        ↳19 PolynomialOrderProcessor (⇒, 0 ms)

        ↳20 intTRS

        ↳21 TerminationGraphProcessor (⇔, 0 ms)

        ↳22 YES

(0) Obligation:

JBC Problem based on JBC Program:

package ConvertRec;

public class ConvertRec {

  public static int convert(List xs, int b) {
    if (xs == null) return 0;
    if (xs.value <= 0) return  b * convert(xs.next, b);
    return 1 + convert(new List(xs.value - 1, xs.next), b);
  }

  public static void main(String[] args) {
    Random.args = args;

    List xs = createList(Random.random());

    convert(xs, Random.random());
  }

  public static List createList(int l) {
	if (l <= 0) {
		return null;
	} else {
		return new List(Random.random(), createList(l-1));
	}
  }
}


package ConvertRec;

public class List {

  int value;
  List next;

  public List() {}

  public List(int value, List next) {
    this.value = value;
    this.next = next;
  }

  public static List copy(List x) {
    if (x == null) return null;
    else return new List(x.value,copy(x.next));
  }
}


package ConvertRec;

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

ConvertRec.ConvertRec.createList(I)LConvertRec/List;: Graph of 158 nodes with 0 SCCs.

ConvertRec.ConvertRec.convert(LConvertRec/List;I)I: Graph of 86 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: ConvertRec.ConvertRec.convert(LConvertRec/List;I)I
SCC calls the following helper methods: ConvertRec.ConvertRec.convert(LConvertRec/List;I)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
- ConvertRec.List: [value, next]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 45 rules for P and 89 rules for R.

P rules:
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub)) → f9560_0_convert_NONNULL(EOS(STATIC_9560), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub))
f9560_0_convert_NONNULL(EOS(STATIC_9560), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub)) → f9563_0_convert_Load(EOS(STATIC_9563), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232)
f9563_0_convert_Load(EOS(STATIC_9563), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232) → f9568_0_convert_FieldAccess(EOS(STATIC_9568), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub))
f9568_0_convert_FieldAccess(EOS(STATIC_9568), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849))) → f9573_0_convert_FieldAccess(EOS(STATIC_9573), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)))
f9573_0_convert_FieldAccess(EOS(STATIC_9573), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849))) → f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, i4239)
f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281) → f9620_0_convert_GT(EOS(STATIC_9620), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281)
f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282) → f9621_0_convert_GT(EOS(STATIC_9621), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282)
f9620_0_convert_GT(EOS(STATIC_9620), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281) → f9624_0_convert_Load(EOS(STATIC_9624), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232) | <=(i4281, 0)
f9624_0_convert_Load(EOS(STATIC_9624), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232) → f9629_0_convert_Load(EOS(STATIC_9629), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232)
f9629_0_convert_Load(EOS(STATIC_9629), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232) → f9635_0_convert_FieldAccess(EOS(STATIC_9635), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)))
f9635_0_convert_FieldAccess(EOS(STATIC_9635), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, java.lang.Object(ConvertRec.List(EOC, i4281, o4849))) → f9639_0_convert_Load(EOS(STATIC_9639), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849)
f9639_0_convert_Load(EOS(STATIC_9639), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849) → f9644_0_convert_InvokeMethod(EOS(STATIC_9644), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232)
f9644_0_convert_InvokeMethod(EOS(STATIC_9644), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232) → f9649_1_convert_InvokeMethod(f9649_0_convert_Load(EOS(STATIC_9649), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232)
f9649_0_convert_Load(EOS(STATIC_9649), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232) → f9655_0_convert_Load(EOS(STATIC_9655), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232)
f9655_0_convert_Load(EOS(STATIC_9655), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232) → f9669_0_convert_Load(EOS(STATIC_9669), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232)
f9669_0_convert_Load(EOS(STATIC_9669), o4876, i232, o4878, o4880, o4876, i232) → f9678_0_convert_Load(EOS(STATIC_9678), o4876, i232, o4878, o4876, i232)
f9678_0_convert_Load(EOS(STATIC_9678), o4876, i232, o4878, o4876, i232) → f9551_0_convert_Load(EOS(STATIC_9551), o4876, i232, o4878, o4876, i232)
f9551_0_convert_Load(EOS(STATIC_9551), o3826, i232, o3828, o3826, i232) → f9558_0_convert_NONNULL(EOS(STATIC_9558), o3826, i232, o3828, o3826, i232, o3826)
f9621_0_convert_GT(EOS(STATIC_9621), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282) → f9627_0_convert_ConstantStackPush(EOS(STATIC_9627), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232) | >(i4282, 0)
f9627_0_convert_ConstantStackPush(EOS(STATIC_9627), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232) → f9632_0_convert_New(EOS(STATIC_9632), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1)
f9632_0_convert_New(EOS(STATIC_9632), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1) → f9637_0_convert_Duplicate(EOS(STATIC_9637), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | =(matching1, 1)
f9637_0_convert_Duplicate(EOS(STATIC_9637), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL))) → f9642_0_convert_Load(EOS(STATIC_9642), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(=(matching1, 1), =(matching2, 0))
f9642_0_convert_Load(EOS(STATIC_9642), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL))) → f9646_0_convert_FieldAccess(EOS(STATIC_9646), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9646_0_convert_FieldAccess(EOS(STATIC_9646), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) → f9651_0_convert_ConstantStackPush(EOS(STATIC_9651), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4282) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9651_0_convert_ConstantStackPush(EOS(STATIC_9651), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4282) → f9657_0_convert_IntArithmetic(EOS(STATIC_9657), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4282, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9657_0_convert_IntArithmetic(EOS(STATIC_9657), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4282, matching4) → f9671_0_convert_Load(EOS(STATIC_9671), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), -(i4282, 1)) | &&(&&(&&(&&(>(i4282, 0), =(matching1, 1)), =(matching2, 0)), =(matching3, 0)), =(matching4, 1))
f9671_0_convert_Load(EOS(STATIC_9671), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283) → f9681_0_convert_FieldAccess(EOS(STATIC_9681), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9681_0_convert_FieldAccess(EOS(STATIC_9681), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) → f9726_0_convert_InvokeMethod(EOS(STATIC_9726), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9726_0_convert_InvokeMethod(EOS(STATIC_9726), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849) → f9729_0__init__Load(EOS(STATIC_9729), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9729_0__init__Load(EOS(STATIC_9729), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849) → f9737_0__init__InvokeMethod(EOS(STATIC_9737), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f9737_0__init__InvokeMethod(EOS(STATIC_9737), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL))) → f9742_0__init__Load(EOS(STATIC_9742), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9742_0__init__Load(EOS(STATIC_9742), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849) → f9825_0__init__Load(EOS(STATIC_9825), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f9825_0__init__Load(EOS(STATIC_9825), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL))) → f9829_0__init__FieldAccess(EOS(STATIC_9829), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9829_0__init__FieldAccess(EOS(STATIC_9829), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL)), i4283) → f9835_0__init__Load(EOS(STATIC_9835), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9835_0__init__Load(EOS(STATIC_9835), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) → f9843_0__init__Load(EOS(STATIC_9843), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL))) | =(matching1, 1)
f9843_0__init__Load(EOS(STATIC_9843), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL))) → f9847_0__init__FieldAccess(EOS(STATIC_9847), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) | =(matching1, 1)
f9847_0__init__FieldAccess(EOS(STATIC_9847), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) → f9951_0__init__Return(EOS(STATIC_9951), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i4283, o4849) | =(matching1, 1)
f9951_0__init__Return(EOS(STATIC_9951), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i4283, o4849) → f9955_0_convert_Load(EOS(STATIC_9955), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849))) | =(matching1, 1)
f9955_0_convert_Load(EOS(STATIC_9955), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849))) → f9959_0_convert_InvokeMethod(EOS(STATIC_9959), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) | =(matching1, 1)
f9959_0_convert_InvokeMethod(EOS(STATIC_9959), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10048_1_convert_InvokeMethod(f10048_0_convert_Load(EOS(STATIC_10048), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) | =(matching1, 1)
f10048_0_convert_Load(EOS(STATIC_10048), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10099_0_convert_Load(EOS(STATIC_10099), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232)
f10099_0_convert_Load(EOS(STATIC_10099), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10121_0_convert_Load(EOS(STATIC_10121), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232)
f10121_0_convert_Load(EOS(STATIC_10121), java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232, o5151, o5149, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232) → f10130_0_convert_Load(EOS(STATIC_10130), java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232, o5151, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232)
f10130_0_convert_Load(EOS(STATIC_10130), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232) → f10142_0_convert_Load(EOS(STATIC_10142), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232)
f10142_0_convert_Load(EOS(STATIC_10142), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232) → f9551_0_convert_Load(EOS(STATIC_9551), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232)
R rules:
f9551_0_convert_Load(EOS(STATIC_9551), o3826, i232, o3828, o3826, i232) → f9558_0_convert_NONNULL(EOS(STATIC_9558), o3826, i232, o3828, o3826, i232, o3826)
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub)) → f9560_0_convert_NONNULL(EOS(STATIC_9560), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub))
f9558_0_convert_NONNULL(EOS(STATIC_9558), NULL, i232, o3828, NULL, i232, NULL) → f9561_0_convert_NONNULL(EOS(STATIC_9561), NULL, i232, o3828, NULL, i232, NULL)
f9560_0_convert_NONNULL(EOS(STATIC_9560), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub)) → f9563_0_convert_Load(EOS(STATIC_9563), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232)
f9561_0_convert_NONNULL(EOS(STATIC_9561), NULL, i232, o3828, NULL, i232, NULL) → f9565_0_convert_ConstantStackPush(EOS(STATIC_9565), NULL, i232, o3828, NULL, i232)
f9563_0_convert_Load(EOS(STATIC_9563), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232) → f9568_0_convert_FieldAccess(EOS(STATIC_9568), java.lang.Object(o4845sub), i232, o3828, java.lang.Object(o4845sub), i232, java.lang.Object(o4845sub))
f9565_0_convert_ConstantStackPush(EOS(STATIC_9565), NULL, i232, o3828, NULL, i232) → f9570_0_convert_Return(EOS(STATIC_9570), NULL, i232, o3828, NULL, i232, 0)
f9568_0_convert_FieldAccess(EOS(STATIC_9568), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849))) → f9573_0_convert_FieldAccess(EOS(STATIC_9573), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)))
f9573_0_convert_FieldAccess(EOS(STATIC_9573), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, java.lang.Object(ConvertRec.List(EOC, i4239, o4849))) → f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4239, o4849)), i232, i4239)
f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281) → f9620_0_convert_GT(EOS(STATIC_9620), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281)
f9578_0_convert_GT(EOS(STATIC_9578), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282) → f9621_0_convert_GT(EOS(STATIC_9621), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282)
f9620_0_convert_GT(EOS(STATIC_9620), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i4281) → f9624_0_convert_Load(EOS(STATIC_9624), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232) | <=(i4281, 0)
f9621_0_convert_GT(EOS(STATIC_9621), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, i4282) → f9627_0_convert_ConstantStackPush(EOS(STATIC_9627), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232) | >(i4282, 0)
f9624_0_convert_Load(EOS(STATIC_9624), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232) → f9629_0_convert_Load(EOS(STATIC_9629), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232)
f9627_0_convert_ConstantStackPush(EOS(STATIC_9627), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232) → f9632_0_convert_New(EOS(STATIC_9632), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1)
f9629_0_convert_Load(EOS(STATIC_9629), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232) → f9635_0_convert_FieldAccess(EOS(STATIC_9635), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)))
f9632_0_convert_New(EOS(STATIC_9632), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1) → f9637_0_convert_Duplicate(EOS(STATIC_9637), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | =(matching1, 1)
f9635_0_convert_FieldAccess(EOS(STATIC_9635), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, java.lang.Object(ConvertRec.List(EOC, i4281, o4849))) → f9639_0_convert_Load(EOS(STATIC_9639), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849)
f9637_0_convert_Duplicate(EOS(STATIC_9637), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL))) → f9642_0_convert_Load(EOS(STATIC_9642), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(=(matching1, 1), =(matching2, 0))
f9639_0_convert_Load(EOS(STATIC_9639), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849) → f9644_0_convert_InvokeMethod(EOS(STATIC_9644), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232)
f9642_0_convert_Load(EOS(STATIC_9642), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL))) → f9646_0_convert_FieldAccess(EOS(STATIC_9646), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9644_0_convert_InvokeMethod(EOS(STATIC_9644), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232) → f9649_1_convert_InvokeMethod(f9649_0_convert_Load(EOS(STATIC_9649), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232), java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), i232, i232, o4849, i232)
f9646_0_convert_FieldAccess(EOS(STATIC_9646), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) → f9651_0_convert_ConstantStackPush(EOS(STATIC_9651), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4282) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9649_0_convert_Load(EOS(STATIC_9649), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232) → f9655_0_convert_Load(EOS(STATIC_9655), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232)
f9651_0_convert_ConstantStackPush(EOS(STATIC_9651), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4282) → f9657_0_convert_IntArithmetic(EOS(STATIC_9657), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4282, 1) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9655_0_convert_Load(EOS(STATIC_9655), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232) → f9669_0_convert_Load(EOS(STATIC_9669), o4849, i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4281, o4849)), o4849, i232)
f9657_0_convert_IntArithmetic(EOS(STATIC_9657), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4282, matching4) → f9671_0_convert_Load(EOS(STATIC_9671), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), -(i4282, 1)) | &&(&&(&&(&&(>(i4282, 0), =(matching1, 1)), =(matching2, 0)), =(matching3, 0)), =(matching4, 1))
f9669_0_convert_Load(EOS(STATIC_9669), o4876, i232, o4878, o4880, o4876, i232) → f9678_0_convert_Load(EOS(STATIC_9678), o4876, i232, o4878, o4876, i232)
f9671_0_convert_Load(EOS(STATIC_9671), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283) → f9681_0_convert_FieldAccess(EOS(STATIC_9681), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9681_0_convert_FieldAccess(EOS(STATIC_9681), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, java.lang.Object(ConvertRec.List(EOC, i4282, o4849))) → f9726_0_convert_InvokeMethod(EOS(STATIC_9726), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9726_0_convert_InvokeMethod(EOS(STATIC_9726), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849) → f9729_0__init__Load(EOS(STATIC_9729), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9727_0_convert_Return(EOS(STATIC_9727), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, i4292, NULL, i4292, NULL, i4292, matching1) → f9732_0_convert_IntArithmetic(EOS(STATIC_9732), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, i4292, 0) | =(matching1, 0)
f9729_0__init__Load(EOS(STATIC_9729), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849) → f9737_0__init__InvokeMethod(EOS(STATIC_9737), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f9732_0_convert_IntArithmetic(EOS(STATIC_9732), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, i4292, matching1) → f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, 0) | =(matching1, 0)
f9737_0__init__InvokeMethod(EOS(STATIC_9737), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL))) → f9742_0__init__Load(EOS(STATIC_9742), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9742_0__init__Load(EOS(STATIC_9742), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849) → f9825_0__init__Load(EOS(STATIC_9825), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f9825_0__init__Load(EOS(STATIC_9825), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL))) → f9829_0__init__FieldAccess(EOS(STATIC_9829), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), o4849, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4283) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9826_0_convert_Return(EOS(STATIC_9826), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, o4959, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, matching1) → f10095_0_convert_Return(EOS(STATIC_10095), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, o4959, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, 0) | =(matching1, 0)
f9829_0__init__FieldAccess(EOS(STATIC_9829), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, matching4, NULL)), o4849, java.lang.Object(ConvertRec.List(EOC, matching5, NULL)), i4283) → f9835_0__init__Load(EOS(STATIC_9835), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) | &&(&&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
f9835_0__init__Load(EOS(STATIC_9835), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) → f9843_0__init__Load(EOS(STATIC_9843), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL))) | =(matching1, 1)
f9843_0__init__Load(EOS(STATIC_9843), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL))) → f9847_0__init__FieldAccess(EOS(STATIC_9847), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) | =(matching1, 1)
f9847_0__init__FieldAccess(EOS(STATIC_9847), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), i4283, o4849, java.lang.Object(ConvertRec.List(EOC, i4283, NULL)), o4849) → f9951_0__init__Return(EOS(STATIC_9951), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i4283, o4849) | =(matching1, 1)
f9951_0__init__Return(EOS(STATIC_9951), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i4283, o4849) → f9955_0_convert_Load(EOS(STATIC_9955), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849))) | =(matching1, 1)
f9955_0_convert_Load(EOS(STATIC_9955), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, i232, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849))) → f9959_0_convert_InvokeMethod(EOS(STATIC_9959), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) | =(matching1, 1)
f9959_0_convert_InvokeMethod(EOS(STATIC_9959), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, matching1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10048_1_convert_InvokeMethod(f10048_0_convert_Load(EOS(STATIC_10048), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232), java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), i232, o3828, 1, java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) | =(matching1, 1)
f10048_0_convert_Load(EOS(STATIC_10048), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10099_0_convert_Load(EOS(STATIC_10099), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232)
f10095_0_convert_Return(EOS(STATIC_10095), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)))), i4498, o5134, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)))), i4498, i4498, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)), i4498, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)), i4498, matching1) → f12400_0_convert_Return(EOS(STATIC_12400), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)))), i4498, o5134, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)))), i4498, i4498, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)), i4498, java.lang.Object(ConvertRec.List(EOC, i4497, o5131)), i4498, 0) | =(matching1, 0)
f10099_0_convert_Load(EOS(STATIC_10099), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232) → f10121_0_convert_Load(EOS(STATIC_10121), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232, o3828, o4849, java.lang.Object(ConvertRec.List(EOC, i4282, o4849)), java.lang.Object(ConvertRec.List(EOC, i4283, o4849)), i232)
f10121_0_convert_Load(EOS(STATIC_10121), java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232, o5151, o5149, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232) → f10130_0_convert_Load(EOS(STATIC_10130), java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232, o5151, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5149)), i232)
f10130_0_convert_Load(EOS(STATIC_10130), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, o5153, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232) → f10142_0_convert_Load(EOS(STATIC_10142), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232)
f10357_0_convert_Return(EOS(STATIC_10357), java.lang.Object(ConvertRec.List(EOC, i4282, NULL)), i4606, o5284, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), i4606, java.lang.Object(ConvertRec.List(EOC, matching3, NULL)), i4606, matching4) → f10398_0_convert_Return(EOS(STATIC_10398), java.lang.Object(ConvertRec.List(EOC, i4282, NULL)), i4606, o5284, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4606, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4606, 0) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f10398_0_convert_Return(EOS(STATIC_10398), java.lang.Object(ConvertRec.List(EOC, i4282, o5318)), i4627, o5321, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, o5318)), i4627, java.lang.Object(ConvertRec.List(EOC, matching3, o5318)), i4627, matching4) → f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, o5318)), i4627, o5321, 1, java.lang.Object(ConvertRec.List(EOC, 0, o5318)), i4627, java.lang.Object(ConvertRec.List(EOC, 0, o5318)), i4627, 0) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, o5811)), i5025, o5814, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, o5811)), i5025, java.lang.Object(ConvertRec.List(EOC, matching3, o5811)), i5025, i5026) → f11148_0_convert_IntArithmetic(EOS(STATIC_11148), java.lang.Object(ConvertRec.List(EOC, i4282, o5811)), i5025, o5814, 1, i5026) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f11094_0_convert_Return(EOS(STATIC_11094), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)))), i5065, o5846, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)))), i5065, i5065, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)), i5065, i5063) → f11779_0_convert_Return(EOS(STATIC_11779), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)))), i5065, o5846, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)))), i5065, i5065, java.lang.Object(ConvertRec.List(EOC, i5064, o5844)), i5065, i5063)
f11135_0_convert_Return(EOS(STATIC_11135), java.lang.Object(ConvertRec.List(EOC, i4282, o5855)), i5081, o5857, matching1, java.lang.Object(ConvertRec.List(EOC, i5082, o5855)), i5081, i5080) → f11831_0_convert_Return(EOS(STATIC_11831), java.lang.Object(ConvertRec.List(EOC, i4282, o5855)), i5081, o5857, 1, java.lang.Object(ConvertRec.List(EOC, i5082, o5855)), i5081, i5080) | =(matching1, 1)
f11148_0_convert_IntArithmetic(EOS(STATIC_11148), java.lang.Object(ConvertRec.List(EOC, i4282, o5811)), i5025, o5814, matching1, i5026) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, i4282, o5811)), i5025, o5814, +(1, i5026)) | &&(>=(i5026, 0), =(matching1, 1))
f11778_0_convert_Return(EOS(STATIC_11778), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, o5969, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, i5211, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)), i5211, i5202) → f11779_0_convert_Return(EOS(STATIC_11779), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, o5969, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, i5211, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)), i5211, i5202)
f11779_0_convert_Return(EOS(STATIC_11779), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, i5448, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)), i5448, i5446) → f11891_0_convert_IntArithmetic(EOS(STATIC_11891), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, i5448, i5446)
f11830_0_convert_Return(EOS(STATIC_11830), java.lang.Object(ConvertRec.List(EOC, i4282, o6004)), i5237, o5997, matching1, java.lang.Object(ConvertRec.List(EOC, i5239, o6004)), i5237, i5226) → f11831_0_convert_Return(EOS(STATIC_11831), java.lang.Object(ConvertRec.List(EOC, i4282, o6004)), i5237, o5997, 1, java.lang.Object(ConvertRec.List(EOC, i5239, o6004)), i5237, i5226) | =(matching1, 1)
f11831_0_convert_Return(EOS(STATIC_11831), java.lang.Object(ConvertRec.List(EOC, i4282, o6252)), i5473, o6254, matching1, java.lang.Object(ConvertRec.List(EOC, i5474, o6252)), i5473, i5472) → f11894_0_convert_IntArithmetic(EOS(STATIC_11894), java.lang.Object(ConvertRec.List(EOC, i4282, o6252)), i5473, o6254, 1, i5472) | =(matching1, 1)
f11891_0_convert_IntArithmetic(EOS(STATIC_11891), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, i5448, i5446) → f11901_0_convert_Return(EOS(STATIC_11901), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, *(i5448, i5446)) | >=(i5446, 1)
f11894_0_convert_IntArithmetic(EOS(STATIC_11894), java.lang.Object(ConvertRec.List(EOC, i4282, o6252)), i5473, o6254, matching1, i5472) → f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, i4282, o6252)), i5473, o6254, +(1, i5472)) | &&(>(i5472, 0), =(matching1, 1))
f11901_0_convert_Return(EOS(STATIC_11901), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, i5520) → f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, o6233, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5447, o6231)))), i5448, i5520)
f12170_0_convert_Return(EOS(STATIC_12170), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, o6423, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, java.lang.Object(ConvertRec.List(EOC, matching3, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, i5617) → f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, o6423, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, i5617) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f12184_0_convert_Return(EOS(STATIC_12184), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, o6493, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, i5701, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)), i5701, i5692) → f11779_0_convert_Return(EOS(STATIC_11779), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, o6493, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, i5701, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)), i5701, i5692)
f12196_0_convert_Return(EOS(STATIC_12196), java.lang.Object(ConvertRec.List(EOC, i4282, o6525)), i5720, o6518, matching1, java.lang.Object(ConvertRec.List(EOC, i5722, o6525)), i5720, i5710) → f11831_0_convert_Return(EOS(STATIC_11831), java.lang.Object(ConvertRec.List(EOC, i4282, o6525)), i5720, o6518, 1, java.lang.Object(ConvertRec.List(EOC, i5722, o6525)), i5720, i5710) | =(matching1, 1)
f12399_0_convert_Return(EOS(STATIC_12399), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, o6615, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, i5796) → f12400_0_convert_Return(EOS(STATIC_12400), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, o6615, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, i5796)
f12400_0_convert_Return(EOS(STATIC_12400), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, i5826, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)), i5826, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)), i5826, i5827) → f12425_0_convert_IntArithmetic(EOS(STATIC_12425), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, i5826, i5827)
f12419_0_convert_Return(EOS(STATIC_12419), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6646sub))), i5820, o6639, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(o6646sub))), i5820, java.lang.Object(ConvertRec.List(EOC, matching3, java.lang.Object(o6646sub))), i5820, i5811) → f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6646sub))), i5820, o6639, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6646sub))), i5820, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6646sub))), i5820, i5811) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f12425_0_convert_IntArithmetic(EOS(STATIC_12425), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, i5826, i5827) → f12432_0_convert_Return(EOS(STATIC_12432), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, *(i5826, i5827))
f12432_0_convert_Return(EOS(STATIC_12432), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, i5866) → f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, o6655, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5825, o6652)))), i5826, i5866)
f12624_0_convert_Return(EOS(STATIC_12624), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, o6802, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, java.lang.Object(ConvertRec.List(EOC, matching3, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, i5962) → f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, o6802, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, i5962) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f12786_0_convert_Return(EOS(STATIC_12786), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, o6884, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, i6044) → f12400_0_convert_Return(EOS(STATIC_12400), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, o6884, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, i6044)
f12801_0_convert_Return(EOS(STATIC_12801), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6914sub))), i6069, o6907, matching1, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(o6914sub))), i6069, java.lang.Object(ConvertRec.List(EOC, matching3, java.lang.Object(o6914sub))), i6069, i6059) → f11030_0_convert_Return(EOS(STATIC_11030), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6914sub))), i6069, o6907, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6914sub))), i6069, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6914sub))), i6069, i6059) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 0))
f9678_0_convert_Load(EOS(STATIC_9678), o4876, i232, o4878, o4876, i232) → f9551_0_convert_Load(EOS(STATIC_9551), o4876, i232, o4878, o4876, i232)
f10142_0_convert_Load(EOS(STATIC_10142), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232) → f9551_0_convert_Load(EOS(STATIC_9551), java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232, o5151, java.lang.Object(ConvertRec.List(EOC, i4283, o5151)), i232)
f9649_1_convert_InvokeMethod(f9570_0_convert_Return(EOS(STATIC_9570), NULL, i4292, o4903, NULL, i4292, matching1), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, i4292, NULL, i4292) → f9727_0_convert_Return(EOS(STATIC_9727), java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, o4903, java.lang.Object(ConvertRec.List(EOC, i4281, NULL)), i4292, i4292, NULL, i4292, NULL, i4292, 0) | =(matching1, 0)
f9649_1_convert_InvokeMethod(f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, o4959, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, matching1), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, o4959, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358) → f9826_0_convert_Return(EOS(STATIC_9826), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, o4959, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)))), i4358, i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, java.lang.Object(ConvertRec.List(EOC, i4351, NULL)), i4358, 0) | =(matching1, 0)
f9649_1_convert_InvokeMethod(f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, i5204, o5962)), i5211, o5969, i5202), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, o5969, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, i5211, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)), i5211) → f11778_0_convert_Return(EOS(STATIC_11778), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, o5969, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)))), i5211, i5211, java.lang.Object(ConvertRec.List(EOC, i5204, o5962)), i5211, i5202)
f9649_1_convert_InvokeMethod(f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, i5694, o6486)), i5701, o6493, i5692), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, o6493, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, i5701, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)), i5701) → f12184_0_convert_Return(EOS(STATIC_12184), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, o6493, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)))), i5701, i5701, java.lang.Object(ConvertRec.List(EOC, i5694, o6486)), i5701, i5692)
f9649_1_convert_InvokeMethod(f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, o6615, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, i5796), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, o6615, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805) → f12399_0_convert_Return(EOS(STATIC_12399), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, o6615, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))))), i5805, i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, java.lang.Object(ConvertRec.List(EOC, i5798, java.lang.Object(o6608sub))), i5805, i5796)
f9649_1_convert_InvokeMethod(f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, o6884, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, i6044), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, o6884, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053) → f12786_0_convert_Return(EOS(STATIC_12786), java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, o6884, java.lang.Object(ConvertRec.List(EOC, i4281, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))))), i6053, i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, java.lang.Object(ConvertRec.List(EOC, i6046, java.lang.Object(o6877sub))), i6053, i6044)
f10048_1_convert_InvokeMethod(f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, matching1, NULL)), i4606, o5284, java.lang.Object(ConvertRec.List(EOC, matching2, NULL)), i4606, matching3), java.lang.Object(ConvertRec.List(EOC, i4282, NULL)), i4606, o5284, matching4, java.lang.Object(ConvertRec.List(EOC, matching5, NULL)), i4606) → f10357_0_convert_Return(EOS(STATIC_10357), java.lang.Object(ConvertRec.List(EOC, i4282, NULL)), i4606, o5284, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4606, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), i4606, 0) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 1)), =(matching5, 0))
f10048_1_convert_InvokeMethod(f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, i5239, o6004)), i5237, o5997, i5226), java.lang.Object(ConvertRec.List(EOC, i4282, o6004)), i5237, o5997, matching1, java.lang.Object(ConvertRec.List(EOC, i5239, o6004)), i5237) → f11830_0_convert_Return(EOS(STATIC_11830), java.lang.Object(ConvertRec.List(EOC, i4282, o6004)), i5237, o5997, 1, java.lang.Object(ConvertRec.List(EOC, i5239, o6004)), i5237, i5226) | =(matching1, 1)
f10048_1_convert_InvokeMethod(f11901_0_convert_Return(EOS(STATIC_11901), java.lang.Object(ConvertRec.List(EOC, matching1, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, o6423, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, i5617), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, o6423, matching3, java.lang.Object(ConvertRec.List(EOC, matching4, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628) → f12170_0_convert_Return(EOS(STATIC_12170), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, o6423, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5621, o6414)))), i5628, i5617) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 0))
f10048_1_convert_InvokeMethod(f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, i5722, o6525)), i5720, o6518, i5710), java.lang.Object(ConvertRec.List(EOC, i4282, o6525)), i5720, o6518, matching1, java.lang.Object(ConvertRec.List(EOC, i5722, o6525)), i5720) → f12196_0_convert_Return(EOS(STATIC_12196), java.lang.Object(ConvertRec.List(EOC, i4282, o6525)), i5720, o6518, 1, java.lang.Object(ConvertRec.List(EOC, i5722, o6525)), i5720, i5710) | =(matching1, 1)
f10048_1_convert_InvokeMethod(f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, matching1, java.lang.Object(o6646sub))), i5820, o6639, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(o6646sub))), i5820, i5811), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6646sub))), i5820, o6639, matching3, java.lang.Object(ConvertRec.List(EOC, matching4, java.lang.Object(o6646sub))), i5820) → f12419_0_convert_Return(EOS(STATIC_12419), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6646sub))), i5820, o6639, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6646sub))), i5820, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6646sub))), i5820, i5811) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 0))
f10048_1_convert_InvokeMethod(f12432_0_convert_Return(EOS(STATIC_12432), java.lang.Object(ConvertRec.List(EOC, matching1, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, o6802, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, i5962), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, o6802, matching3, java.lang.Object(ConvertRec.List(EOC, matching4, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974) → f12624_0_convert_Return(EOS(STATIC_12624), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, o6802, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, i5966, o6794)))), i5974, i5962) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 0))
f10048_1_convert_InvokeMethod(f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, matching1, java.lang.Object(o6914sub))), i6069, o6907, java.lang.Object(ConvertRec.List(EOC, matching2, java.lang.Object(o6914sub))), i6069, i6059), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6914sub))), i6069, o6907, matching3, java.lang.Object(ConvertRec.List(EOC, matching4, java.lang.Object(o6914sub))), i6069) → f12801_0_convert_Return(EOS(STATIC_12801), java.lang.Object(ConvertRec.List(EOC, i4282, java.lang.Object(o6914sub))), i6069, o6907, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6914sub))), i6069, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(o6914sub))), i6069, i6059) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 0))

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

P rules:
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, java.lang.Object(ConvertRec.List(EOC, x0, x1))) → f9649_1_convert_InvokeMethod(f9558_0_convert_NONNULL(EOS(STATIC_9558), x1, x2, x3, x1, x2, x1), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x2, x1, x2) | <=(x0, 0)
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x1, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, java.lang.Object(ConvertRec.List(EOC, x0, x1))) → f10048_1_convert_InvokeMethod(f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2, x1, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1))), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x1, 1, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2) | >(x0, 0)
R rules:
f9558_0_convert_NONNULL(EOS(STATIC_9558), NULL, x0, x1, NULL, x0, NULL) → f9570_0_convert_Return(EOS(STATIC_9570), NULL, x0, x1, NULL, x0, 0)
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, java.lang.Object(ConvertRec.List(EOC, x0, x1))) → f9649_1_convert_InvokeMethod(f9558_0_convert_NONNULL(EOS(STATIC_9558), x1, x2, x3, x1, x2, x1), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x2, x1, x2) | <=(x0, 0)
f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x1, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, java.lang.Object(ConvertRec.List(EOC, x0, x1))) → f10048_1_convert_InvokeMethod(f9558_0_convert_NONNULL(EOS(STATIC_9558), java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2, x1, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1))), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x1, 1, java.lang.Object(ConvertRec.List(EOC, -(x0, 1), x1)), x2) | >(x0, 0)
f9649_1_convert_InvokeMethod(f9570_0_convert_Return(EOS(STATIC_9570), NULL, x0, x1, NULL, x0, 0), java.lang.Object(ConvertRec.List(EOC, x3, NULL)), x0, x1, java.lang.Object(ConvertRec.List(EOC, x3, NULL)), x0, x0, NULL, x0) → f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, x3, NULL)), x0, x1, java.lang.Object(ConvertRec.List(EOC, x3, NULL)), x0, 0)
f9649_1_convert_InvokeMethod(f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, x0, NULL)), x1, x2, java.lang.Object(ConvertRec.List(EOC, x0, NULL)), x1, 0), java.lang.Object(ConvertRec.List(EOC, x4, java.lang.Object(ConvertRec.List(EOC, x0, NULL)))), x1, x2, java.lang.Object(ConvertRec.List(EOC, x4, java.lang.Object(ConvertRec.List(EOC, x0, NULL)))), x1, x1, java.lang.Object(ConvertRec.List(EOC, x0, NULL)), x1) → f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, x4, java.lang.Object(ConvertRec.List(EOC, x0, NULL)))), x1, x2, java.lang.Object(ConvertRec.List(EOC, x4, java.lang.Object(ConvertRec.List(EOC, x0, NULL)))), x1, 0)
f9649_1_convert_InvokeMethod(f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, x4), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x2, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2) → f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, *(x2, x4)) | >(+(x4, 1), 1)
f9649_1_convert_InvokeMethod(f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, x4), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x2, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2) → f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, x1)))), x2, *(x2, x4)) | >(+(x4, 1), 1)
f9649_1_convert_InvokeMethod(f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2, x4), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x2, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2) → f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, *(x2, x4))
f9649_1_convert_InvokeMethod(f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2, x4), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x2, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))), x2) → f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, x3, java.lang.Object(ConvertRec.List(EOC, x5, java.lang.Object(ConvertRec.List(EOC, x0, java.lang.Object(x1))))), x2, *(x2, x4))
f10048_1_convert_InvokeMethod(f9735_0_convert_Return(EOS(STATIC_9735), java.lang.Object(ConvertRec.List(EOC, 0, NULL)), x1, x2, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), x1, 0), java.lang.Object(ConvertRec.List(EOC, x5, NULL)), x1, x2, 1, java.lang.Object(ConvertRec.List(EOC, 0, NULL)), x1) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x5, NULL)), x1, x2, 1)
f10048_1_convert_InvokeMethod(f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, x4), java.lang.Object(ConvertRec.List(EOC, x5, x1)), x2, x3, 1, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2) → f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, x5, x1)), x2, x3, +(1, x4)) | >(x4, 0)
f10048_1_convert_InvokeMethod(f11901_0_convert_Return(EOS(STATIC_11901), java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x6), java.lang.Object(ConvertRec.List(EOC, x7, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x7, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, +(1, x6)) | >(+(x6, 1), 0)
f10048_1_convert_InvokeMethod(f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2, x3, x4), java.lang.Object(ConvertRec.List(EOC, x5, x1)), x2, x3, 1, java.lang.Object(ConvertRec.List(EOC, x0, x1)), x2) → f11907_0_convert_Return(EOS(STATIC_11907), java.lang.Object(ConvertRec.List(EOC, x5, x1)), x2, x3, +(1, x4)) | >(x4, 0)
f10048_1_convert_InvokeMethod(f12155_0_convert_Return(EOS(STATIC_12155), java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2, x3, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2, x5), java.lang.Object(ConvertRec.List(EOC, x6, java.lang.Object(x1))), x2, x3, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x6, java.lang.Object(x1))), x2, x3, +(1, x5)) | >(+(x5, 1), 0)
f10048_1_convert_InvokeMethod(f12432_0_convert_Return(EOS(STATIC_12432), java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x6), java.lang.Object(ConvertRec.List(EOC, x7, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x7, java.lang.Object(ConvertRec.List(EOC, x1, x2)))), x3, x4, +(1, x6)) | >(+(x6, 1), 0)
f10048_1_convert_InvokeMethod(f12606_0_convert_Return(EOS(STATIC_12606), java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2, x3, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2, x5), java.lang.Object(ConvertRec.List(EOC, x6, java.lang.Object(x1))), x2, x3, 1, java.lang.Object(ConvertRec.List(EOC, 0, java.lang.Object(x1))), x2) → f11176_0_convert_Return(EOS(STATIC_11176), java.lang.Object(ConvertRec.List(EOC, x6, java.lang.Object(x1))), x2, x3, +(1, x5)) | >(+(x5, 1), 0)

Filtered ground terms:

f9558_0_convert_NONNULL(x1, x2, x3, x4, x5, x6, x7) → f9558_0_convert_NONNULL(x2, x3, x4, x5, x6, x7)
Cond_f9558_0_convert_NONNULL(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f9558_0_convert_NONNULL(x1, x3, x4, x5, x6, x7, x8)
Cond_f9558_0_convert_NONNULL1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f9558_0_convert_NONNULL1(x1, x3, x4, x5, x6, x7, x8)
f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x6, x7)
ConvertRec.List(x1, x2, x3) → ConvertRec.List(x2, x3)
f9570_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f9570_0_convert_Return(x3, x4, x6)
f9735_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f9735_0_convert_Return(x2, x3, x4, x5, x6)
f12606_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f12606_0_convert_Return(x2, x3, x4, x5, x6, x7)
f12155_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f12155_0_convert_Return(x2, x3, x4, x5, x6, x7)
f11176_0_convert_Return(x1, x2, x3, x4, x5) → f11176_0_convert_Return(x2, x3, x4, x5)
Cond_f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x7, x8)
f11907_0_convert_Return(x1, x2, x3, x4, x5) → f11907_0_convert_Return(x2, x3, x4, x5)
Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x7, x8)
Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3, x4, x5, x7, x8)
Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3, x4, x5, x7, x8)
Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3, x4, x5, x7, x8)
Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3, x4, x5, x7, x8)
f11901_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f11901_0_convert_Return(x2, x3, x4, x5, x6, x7)
f12432_0_convert_Return(x1, x2, x3, x4, x5, x6, x7) → f12432_0_convert_Return(x2, x3, x4, x5, x6, x7)

Filtered unneeded arguments:

f9649_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f9649_1_convert_InvokeMethod(x1, x2, x3, x5, x6, x7, x8, x9)
f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6) → f10048_1_convert_InvokeMethod(x1, x2, x3, x5, x6)
f9570_0_convert_Return(x1, x2, x3) → f9570_0_convert_Return(x1, x3)
f9735_0_convert_Return(x1, x2, x3, x4, x5) → f9735_0_convert_Return(x1, x2, x4, x5)
f11176_0_convert_Return(x1, x2, x3, x4) → f11176_0_convert_Return(x1, x2, x4)
Cond_f9649_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f9649_1_convert_InvokeMethod(x1, x2, x3, x4, x6, x7, x8, x9, x10)
Cond_f9649_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f9649_1_convert_InvokeMethod1(x1, x2, x3, x4, x6, x7, x8, x9, x10)
f12155_0_convert_Return(x1, x2, x3, x4, x5, x6) → f12155_0_convert_Return(x1, x2, x4, x5, x6)
f12606_0_convert_Return(x1, x2, x3, x4, x5, x6) → f12606_0_convert_Return(x1, x2, x4, x5, x6)
Cond_f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x6, x7)
f11901_0_convert_Return(x1, x2, x3, x4, x5, x6) → f11901_0_convert_Return(x1, x2, x4, x5, x6)
Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3, x4, x6, x7)
Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3, x4, x6, x7)
Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3, x4, x6, x7)
f12432_0_convert_Return(x1, x2, x3, x4, x5, x6) → f12432_0_convert_Return(x1, x2, x4, x5, x6)
Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3, x4, x6, x7)
Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3, x4, x5, x6, x7) → Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3, x4, x6, x7)
f11907_0_convert_Return(x1, x2, x3, x4) → f11907_0_convert_Return(x1, x2, x4)

Filtered duplicate args:

f9558_0_convert_NONNULL(x1, x2, x3, x4, x5, x6) → f9558_0_convert_NONNULL(x3, x5, x6)
Cond_f9558_0_convert_NONNULL(x1, x2, x3, x4, x5, x6, x7) → Cond_f9558_0_convert_NONNULL(x1, x4, x6, x7)
f9649_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → f9649_1_convert_InvokeMethod(x1, x4)
Cond_f9558_0_convert_NONNULL1(x1, x2, x3, x4, x5, x6, x7) → Cond_f9558_0_convert_NONNULL1(x1, x6, x7)
f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5) → f10048_1_convert_InvokeMethod(x1, x2)
f9570_0_convert_Return(x1, x2) → f9570_0_convert_Return(x2)
f9735_0_convert_Return(x1, x2, x3, x4) → f9735_0_convert_Return(x3, x4)
f12606_0_convert_Return(x1, x2, x3, x4, x5) → f12606_0_convert_Return(x3, x4, x5)
Cond_f9649_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f9649_1_convert_InvokeMethod(x1, x2, x5)
f12155_0_convert_Return(x1, x2, x3, x4, x5) → f12155_0_convert_Return(x3, x4, x5)
Cond_f9649_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f9649_1_convert_InvokeMethod1(x1, x2, x5)
Cond_f10048_1_convert_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod(x1, x2, x3)
f11901_0_convert_Return(x1, x2, x3, x4, x5) → f11901_0_convert_Return(x3, x4, x5)
Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod1(x1, x2, x3)
Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod2(x1, x2, x3)
Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod3(x1, x2, x3)
f12432_0_convert_Return(x1, x2, x3, x4, x5) → f12432_0_convert_Return(x3, x4, x5)
Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod4(x1, x2, x3)
Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3, x4, x5, x6) → Cond_f10048_1_convert_InvokeMethod5(x1, x2, x3)

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

P rules:
F9558_0_CONVERT_NONNULL(x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL(x3, x2, x1) | <=(x0, 0)
F9558_0_CONVERT_NONNULL(x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL(x1, x2, java.lang.Object(ConvertRec.List(-(x0, 1), x1))) | >(x0, 0)
R rules:

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

P rules:
F9558_0_CONVERT_NONNULL'(x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL(<=(x0, 0), x3, x2, java.lang.Object(ConvertRec.List(x0, x1)))
COND_F9558_0_CONVERT_NONNULL(TRUE, x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x3, x2, x1)
F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL1(>(x0, 0), x1, x2, java.lang.Object(ConvertRec.List(x0, x1)))
COND_F9558_0_CONVERT_NONNULL1(TRUE, x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(-(x0, 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:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(x0[0] <= 0, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))
(1): COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])
(2): F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(x0[2] > 0, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))
(3): COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3] - 1, x1[3])))

(0) -> (1), if (x0[0] <= 0 ∧x3[0] →^* x3[1]∧x2[0] →^* x2[1]∧java.lang.Object(ConvertRec.List(x0[0], x1[0])) →^* java.lang.Object(ConvertRec.List(x0[1], x1[1])))

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

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

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

(3) -> (0), if (x1[3] →^* x3[0]∧x2[3] →^* x2[0]∧java.lang.Object(ConvertRec.List(x0[3] - 1, x1[3])) →^* java.lang.Object(ConvertRec.List(x0[0], x1[0])))

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

The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: true Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@32f452d1 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair F9558_0_CONVERT_NONNULL'(x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL(<=(x0, 0), x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))), COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1]) which results in the following constraint:
(1)    (<=(x0[0], 0)=TRUE∧x3[0]=x3[1]∧x2[0]=x2[1]∧java.lang.Object(ConvertRec.List(x0[0], x1[0]))=java.lang.Object(ConvertRec.List(x0[1], x1[1])) ⇒ F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))≥COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (<=(x0[0], 0)=TRUE ⇒ F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))≥COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥)∧[(3)bni_20 + (-1)Bound*bni_20] + [(4)bni_20]x1[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥)∧[(3)bni_20 + (-1)Bound*bni_20] + [(4)bni_20]x1[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥)∧[(3)bni_20 + (-1)Bound*bni_20] + [(4)bni_20]x1[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥)∧[(4)bni_20] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_20 + (-1)Bound*bni_20] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)

For Pair COND_F9558_0_CONVERT_NONNULL(TRUE, x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x3, x2, x1) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))), COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1]), F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) which results in the following constraint:
(7)    (<=(x0[0], 0)=TRUE∧x3[0]=x3[1]∧x2[0]=x2[1]∧java.lang.Object(ConvertRec.List(x0[0], x1[0]))=java.lang.Object(ConvertRec.List(x0[1], x1[1]))∧x3[1]=x3[0]1∧x2[1]=x2[0]1∧x1[1]=java.lang.Object(ConvertRec.List(x0[0]1, x1[0]1)) ⇒ COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1])))≥F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥))

We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
(8)    (<=(x0[0], 0)=TRUE ⇒ COND_F9558_0_CONVERT_NONNULL(TRUE, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], java.lang.Object(ConvertRec.List(x0[0]1, x1[0]1)))))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL(TRUE, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], java.lang.Object(ConvertRec.List(x0[0]1, x1[0]1)))))≥F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0]1, x1[0]1)))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x1[0]1 ≥ 0∧[16 + (-1)bso_23] + [12]x1[0]1 ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x1[0]1 ≥ 0∧[16 + (-1)bso_23] + [12]x1[0]1 ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x1[0]1 ≥ 0∧[16 + (-1)bso_23] + [12]x1[0]1 ≥ 0)

We simplified constraint (11) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(16)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(19)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_23] ≥ 0∧[1] ≥ 0)
We consider the chain F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))), COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1]), F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) which results in the following constraint:
(13)    (<=(x0[0], 0)=TRUE∧x3[0]=x3[1]∧x2[0]=x2[1]∧java.lang.Object(ConvertRec.List(x0[0], x1[0]))=java.lang.Object(ConvertRec.List(x0[1], x1[1]))∧x3[1]=x1[2]∧x2[1]=x2[2]∧x1[1]=java.lang.Object(ConvertRec.List(x0[2], x1[2])) ⇒ COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1])))≥F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥))

We simplified constraint (13) using rules (I), (II), (III), (IV) which results in the following new constraint:
(14)    (<=(x0[0], 0)=TRUE ⇒ COND_F9558_0_CONVERT_NONNULL(TRUE, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], java.lang.Object(ConvertRec.List(x0[2], x3[0])))))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL(TRUE, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], java.lang.Object(ConvertRec.List(x0[2], x3[0])))))≥F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[2], x3[0])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x3[0] ≥ 0∧[16 + (-1)bso_23] + [12]x3[0] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x3[0] ≥ 0∧[16 + (-1)bso_23] + [12]x3[0] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(19)bni_22 + (-1)Bound*bni_22] + [(16)bni_22]x3[0] ≥ 0∧[16 + (-1)bso_23] + [12]x3[0] ≥ 0)

We simplified constraint (17) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(16)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(19)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_23] ≥ 0∧[1] ≥ 0)

For Pair F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL1(>(x0, 0), x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))), COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))) which results in the following constraint:
(19)    (>(x0[2], 0)=TRUE∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(ConvertRec.List(x0[2], x1[2]))=java.lang.Object(ConvertRec.List(x0[3], x1[3])) ⇒ F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥))

We simplified constraint (19) using rules (I), (II), (IV) which results in the following new constraint:
(20)    (>(x0[2], 0)=TRUE ⇒ F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(3)bni_24 + (-1)Bound*bni_24] + [(4)bni_24]x1[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(3)bni_24 + (-1)Bound*bni_24] + [(4)bni_24]x1[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(3)bni_24 + (-1)Bound*bni_24] + [(4)bni_24]x1[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(4)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_25] ≥ 0)

For Pair COND_F9558_0_CONVERT_NONNULL1(TRUE, x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(-(x0, 1), x1))) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))), COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))), F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) which results in the following constraint:
(25)    (>(x0[2], 0)=TRUE∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(ConvertRec.List(x0[2], x1[2]))=java.lang.Object(ConvertRec.List(x0[3], x1[3]))∧x1[3]=x3[0]∧x2[3]=x2[0]∧java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))=java.lang.Object(ConvertRec.List(x0[0], x1[0])) ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (25) using rules (I), (II), (III), (IV) which results in the following new constraint:
(26)    (>(x0[2], 0)=TRUE ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(-(x0[2], 1), x1[2])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(4)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)
We consider the chain F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))), COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))), F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) which results in the following constraint:
(31)    (>(x0[2], 0)=TRUE∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(ConvertRec.List(x0[2], x1[2]))=java.lang.Object(ConvertRec.List(x0[3], x1[3]))∧x1[3]=x1[2]1∧x2[3]=x2[2]1∧java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))=java.lang.Object(ConvertRec.List(x0[2]1, x1[2]1)) ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (31) using rules (I), (II), (III), (IV) which results in the following new constraint:
(32)    (>(x0[2], 0)=TRUE ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(-(x0[2], 1), x1[2])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [(4)bni_26]x1[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(4)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)

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

F9558_0_CONVERT_NONNULL'(x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL(<=(x0, 0), x3, x2, java.lang.Object(ConvertRec.List(x0, x1)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))), ≥)∧[(4)bni_20] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_20 + (-1)Bound*bni_20] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)
COND_F9558_0_CONVERT_NONNULL(TRUE, x3, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x3, x2, x1)
- (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(16)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(19)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_23] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])), ≥)∧[(16)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(19)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[16 + (-1)bso_23] ≥ 0∧[1] ≥ 0)
F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → COND_F9558_0_CONVERT_NONNULL1(>(x0, 0), x1, x2, java.lang.Object(ConvertRec.List(x0, x1)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(4)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_25] ≥ 0)
COND_F9558_0_CONVERT_NONNULL1(TRUE, x1, x2, java.lang.Object(ConvertRec.List(x0, x1))) → F9558_0_CONVERT_NONNULL'(x1, x2, java.lang.Object(ConvertRec.List(-(x0, 1), x1)))
- (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(4)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(4)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(F9558_0_CONVERT_NONNULL'(x₁, x₂, x₃)) = [-1] + x₃
POL(java.lang.Object(x₁)) = [2]x₁
POL(ConvertRec.List(x₁, x₂)) = [2] + [2]x₂
POL(COND_F9558_0_CONVERT_NONNULL(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(<=(x₁, x₂)) = 0
POL(0) = 0
POL(COND_F9558_0_CONVERT_NONNULL1(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(>(x₁, x₂)) = 0
POL(-(x₁, x₂)) = 0
POL(1) = 0

The following pairs are in P_>:

COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])

The following pairs are in P_bound:

F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))
COND_F9558_0_CONVERT_NONNULL(TRUE, x3[1], x2[1], java.lang.Object(ConvertRec.List(x0[1], x1[1]))) → F9558_0_CONVERT_NONNULL'(x3[1], x2[1], x1[1])
F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))
COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))

The following pairs are in P_≥:

F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(<=(x0[0], 0), x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))
F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))
COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))

There are no usable rules.

(9) Obligation:

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

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): F9558_0_CONVERT_NONNULL'(x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0]))) → COND_F9558_0_CONVERT_NONNULL(x0[0] <= 0, x3[0], x2[0], java.lang.Object(ConvertRec.List(x0[0], x1[0])))
(2): F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(x0[2] > 0, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))
(3): COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3] - 1, x1[3])))

(3) -> (0), if (x1[3] →^* x3[0]∧x2[3] →^* x2[0]∧java.lang.Object(ConvertRec.List(x0[3] - 1, x1[3])) →^* java.lang.Object(ConvertRec.List(x0[0], x1[0])))

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

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

The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) Obligation:

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

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3] - 1, x1[3])))
(2): F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(x0[2] > 0, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))

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

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

The set Q is empty.

(12) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@483beacd Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))), COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))), F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) which results in the following constraint:
(1)    (>(x0[2], 0)=TRUE∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(ConvertRec.List(x0[2], x1[2]))=java.lang.Object(ConvertRec.List(x0[3], x1[3]))∧x1[3]=x1[2]1∧x2[3]=x2[2]1∧java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))=java.lang.Object(ConvertRec.List(x0[2]1, x1[2]1)) ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3])))≥F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (1) using rules (I), (II), (III), (IV) which results in the following new constraint:
(2)    (>(x0[2], 0)=TRUE ⇒ COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(-(x0[2], 1), x1[2])))∧(U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(-3)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(-3)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧[(-3)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧0 = 0∧0 = 0∧[(-3)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x0[2] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) the following chains were created:

We consider the chain F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))), COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3]))) which results in the following constraint:
(8)    (>(x0[2], 0)=TRUE∧x1[2]=x1[3]∧x2[2]=x2[3]∧java.lang.Object(ConvertRec.List(x0[2], x1[2]))=java.lang.Object(ConvertRec.List(x0[3], x1[3])) ⇒ F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥))

We simplified constraint (8) using rules (I), (II), (IV) which results in the following new constraint:
(9)    (>(x0[2], 0)=TRUE ⇒ F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥NonInfC∧F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))≥COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))∧(U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(-3)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(-3)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧[(-3)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧0 = 0∧0 = 0∧[(-3)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

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

COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))
- (x0[2] ≥ 0 ⇒ (U^Increasing(F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_20 + (-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_F9558_0_CONVERT_NONNULL1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + x₂
POL(java.lang.Object(x₁)) = [1] + [-1]x₁
POL(ConvertRec.List(x₁, x₂)) = [-1] + [-1]x₂ + x₁
POL(F9558_0_CONVERT_NONNULL'(x₁, x₂, x₃)) = [-1] + [-1]x₃ + x₁
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(1) = [1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0

The following pairs are in P_>:

COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))

The following pairs are in P_bound:

COND_F9558_0_CONVERT_NONNULL1(TRUE, x1[3], x2[3], java.lang.Object(ConvertRec.List(x0[3], x1[3]))) → F9558_0_CONVERT_NONNULL'(x1[3], x2[3], java.lang.Object(ConvertRec.List(-(x0[3], 1), x1[3])))
F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))

The following pairs are in P_≥:

F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(>(x0[2], 0), x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))

There are no usable rules.

(13) Obligation:

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

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): F9558_0_CONVERT_NONNULL'(x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2]))) → COND_F9558_0_CONVERT_NONNULL1(x0[2] > 0, x1[2], x2[2], java.lang.Object(ConvertRec.List(x0[2], x1[2])))

The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(16) Obligation:

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

Used field analysis yielded the following read fields:
- java.lang.String: [count]
Marker field analysis yielded the following relations that could be markers:

(17) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 53 IRules

P rules:
f1909_0_createList_GT(EOS, i574, i574, i574) → f1918_0_createList_GT(EOS, i574, i574, i574)
f1918_0_createList_GT(EOS, i574, i574, i574) → f1928_0_createList_New(EOS, i574, i574) | >(i574, 0)
f1928_0_createList_New(EOS, i574, i574) → f1939_0_createList_Duplicate(EOS, i574, i574)
f1939_0_createList_Duplicate(EOS, i574, i574) → f1948_0_createList_InvokeMethod(EOS, i574, i574)
f1948_0_createList_InvokeMethod(EOS, i574, i574) → f1971_0_random_FieldAccess(EOS, i574, i574)
f1971_0_random_FieldAccess(EOS, i574, i574) → f1979_0_random_ArrayLength(EOS, i574, i574, java.lang.Object(ARRAY(i36)))
f1979_0_random_ArrayLength(EOS, i574, i574, java.lang.Object(ARRAY(i36))) → f1982_0_random_FieldAccess(EOS, i574, i574, i36) | >=(i36, 0)
f1982_0_random_FieldAccess(EOS, i574, i574, i36) → f1985_0_random_GT(EOS, i574, i574, i36, i544)
f1985_0_random_GT(EOS, i574, i574, i36, i544) → f1995_0_random_GT(EOS, i574, i574, i36, i544)
f1985_0_random_GT(EOS, i574, i574, i36, i544) → f1996_0_random_GT(EOS, i574, i574, i36, i544)
f1995_0_random_GT(EOS, i574, i574, i36, i544) → f2008_0_random_FieldAccess(EOS, i574, i574) | >(i36, i544)
f2008_0_random_FieldAccess(EOS, i574, i574) → f2031_0_random_FieldAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36)))
f2031_0_random_FieldAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36))) → f2047_0_random_ArrayAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36)), i544)
f2047_0_random_ArrayAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36)), i544) → f2054_0_random_ArrayAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36)), i544)
f2054_0_random_ArrayAccess(EOS, i574, i574, java.lang.Object(ARRAY(i36)), i544) → f2061_0_random_Store(EOS, i574, i574, o705) | <(i544, i36)
f2061_0_random_Store(EOS, i574, i574, o705) → f2070_0_random_FieldAccess(EOS, i574, i574, o705)
f2070_0_random_FieldAccess(EOS, i574, i574, o705) → f2078_0_random_ConstantStackPush(EOS, i574, i574, o705, i544)
f2078_0_random_ConstantStackPush(EOS, i574, i574, o705, i544) → f2087_0_random_IntArithmetic(EOS, i574, i574, o705, i544, 1)
f2087_0_random_IntArithmetic(EOS, i574, i574, o705, i544, matching1) → f2095_0_random_FieldAccess(EOS, i574, i574, o705, +(i544, 1)) | &&(>=(i544, 0), =(matching1, 1))
f2095_0_random_FieldAccess(EOS, i574, i574, o705, i626) → f2107_0_random_Load(EOS, i574, i574, o705)
f2107_0_random_Load(EOS, i574, i574, o705) → f2149_0_random_NONNULL(EOS, i574, i574, o705, o705)
f2149_0_random_NONNULL(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub)) → f2158_0_random_NONNULL(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub))
f2149_0_random_NONNULL(EOS, i574, i574, NULL, NULL) → f2159_0_random_NONNULL(EOS, i574, i574, NULL, NULL)
f2158_0_random_NONNULL(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub)) → f2168_0_random_Load(EOS, i574, i574, java.lang.Object(o726sub))
f2168_0_random_Load(EOS, i574, i574, java.lang.Object(o726sub)) → f2201_0_random_InvokeMethod(EOS, i574, i574, java.lang.Object(o726sub))
f2201_0_random_InvokeMethod(EOS, i574, i574, java.lang.Object(o726sub)) → f2264_0_length_Load(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub))
f2264_0_length_Load(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub)) → f2287_0_length_FieldAccess(EOS, i574, i574, java.lang.Object(o726sub), java.lang.Object(o726sub))
f2287_0_length_FieldAccess(EOS, i574, i574, java.lang.Object(java.lang.String(o800sub, i735)), java.lang.Object(java.lang.String(o800sub, i735))) → f2309_0_length_FieldAccess(EOS, i574, i574, java.lang.Object(java.lang.String(o800sub, i735)), java.lang.Object(java.lang.String(o800sub, i735))) | >=(i735, 0)
f2309_0_length_FieldAccess(EOS, i574, i574, java.lang.Object(java.lang.String(o800sub, i735)), java.lang.Object(java.lang.String(o800sub, i735))) → f2343_0_length_Return(EOS, i574, i574, java.lang.Object(java.lang.String(o800sub, i735)), i735)
f2343_0_length_Return(EOS, i574, i574, java.lang.Object(java.lang.String(o800sub, i735)), i735) → f2370_0_random_Return(EOS, i574, i574, i735)
f2370_0_random_Return(EOS, i574, i574, i735) → f2388_0_createList_Load(EOS, i574, i574, i735)
f2388_0_createList_Load(EOS, i574, i574, i735) → f2417_0_createList_ConstantStackPush(EOS, i574, i735, i574)
f2417_0_createList_ConstantStackPush(EOS, i574, i735, i574) → f2445_0_createList_IntArithmetic(EOS, i574, i735, i574, 1)
f2445_0_createList_IntArithmetic(EOS, i574, i735, i574, matching1) → f2475_0_createList_InvokeMethod(EOS, i574, i735, -(i574, 1)) | &&(>(i574, 0), =(matching1, 1))
f2475_0_createList_InvokeMethod(EOS, i574, i735, i844) → f2496_0_createList_Load(EOS, i844, i844)
f2475_0_createList_InvokeMethod(EOS, i574, i735, i844) → f2496_1_createList_Load(EOS, i574, i735, i844, i844)
f2496_0_createList_Load(EOS, i844, i844) → f2538_0_createList_Load(EOS, i844, i844)
f2538_0_createList_Load(EOS, i844, i844) → f1866_0_createList_Load(EOS, i844, i844)
f1866_0_createList_Load(EOS, i545, i545) → f1909_0_createList_GT(EOS, i545, i545, i545)
f2159_0_random_NONNULL(EOS, i574, i574, NULL, NULL) → f2172_0_random_ConstantStackPush(EOS, i574, i574, NULL)
f2172_0_random_ConstantStackPush(EOS, i574, i574, NULL) → f2212_0_random_Return(EOS, i574, i574, NULL, 0)
f2212_0_random_Return(EOS, i574, i574, NULL, matching1) → f2268_0_createList_Load(EOS, i574, i574, 0) | =(matching1, 0)
f2268_0_createList_Load(EOS, i574, i574, matching1) → f2388_0_createList_Load(EOS, i574, i574, 0) | =(matching1, 0)
f1996_0_random_GT(EOS, i574, i574, i36, i544) → f2020_0_random_ConstantStackPush(EOS, i574, i574) | <=(i36, i544)
f2020_0_random_ConstantStackPush(EOS, i574, i574) → f2039_0_random_Return(EOS, i574, i574, 0)
f2039_0_random_Return(EOS, i574, i574, matching1) → f2052_0_createList_Load(EOS, i574, i574, 0) | =(matching1, 0)
f2052_0_createList_Load(EOS, i574, i574, matching1) → f2058_0_createList_ConstantStackPush(EOS, i574, 0, i574) | =(matching1, 0)
f2058_0_createList_ConstantStackPush(EOS, i574, matching1, i574) → f2067_0_createList_IntArithmetic(EOS, i574, 0, i574, 1) | =(matching1, 0)
f2067_0_createList_IntArithmetic(EOS, i574, matching1, i574, matching2) → f2075_0_createList_InvokeMethod(EOS, i574, 0, -(i574, 1)) | &&(&&(>(i574, 0), =(matching1, 0)), =(matching2, 1))
f2075_0_createList_InvokeMethod(EOS, i574, matching1, i625) → f2084_0_createList_Load(EOS, i625, i625) | =(matching1, 0)
f2075_0_createList_InvokeMethod(EOS, i574, matching1, i625) → f2084_1_createList_Load(EOS, i574, 0, i625, i625) | =(matching1, 0)
f2084_0_createList_Load(EOS, i625, i625) → f2094_0_createList_Load(EOS, i625, i625)
f2094_0_createList_Load(EOS, i625, i625) → f1866_0_createList_Load(EOS, i625, i625)

Combined rules. Obtained 6 IRules

P rules:
f2475_0_createList_InvokeMethod(EOS, i574, i735, i844) → f2496_1_createList_Load(EOS, i574, i735, i844, i844)
f1909_0_createList_GT(EOS, x0, x0, x0) → f2475_0_createList_InvokeMethod(EOS, x0, x1, -(x0, 1)) | &&(>(+(x1, 1), 0), >(x0, 0))
f2475_0_createList_InvokeMethod(EOS, x0, x1, x2) → f1909_0_createList_GT(EOS, x2, x2, x2)
f1909_0_createList_GT(EOS, x0, x0, x0) → f2475_0_createList_InvokeMethod(EOS, x0, 0, -(x0, 1)) | >(x0, 0)
f1909_0_createList_GT(EOS, x0, x0, x0) → f2084_1_createList_Load(EOS, x0, 0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f1909_0_createList_GT(EOS, x0, x0, x0) → f1909_0_createList_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f2475_0_createList_InvokeMethod(x1, x2, x3, x4) → f2475_0_createList_InvokeMethod(x2, x3, x4)
f2496_1_createList_Load(x1, x2, x3, x4, x5) → f2496_1_createList_Load(x2, x3, x4, x5)
f1909_0_createList_GT(x1, x2, x3, x4) → f1909_0_createList_GT(x2, x3, x4)
Cond_f1909_0_createList_GT(x1, x2, x3, x4, x5, x6) → Cond_f1909_0_createList_GT(x1, x3, x4, x5, x6)
Cond_f1909_0_createList_GT1(x1, x2, x3, x4, x5) → Cond_f1909_0_createList_GT1(x1, x3, x4, x5)
Cond_f1909_0_createList_GT2(x1, x2, x3, x4, x5) → Cond_f1909_0_createList_GT2(x1, x3, x4, x5)
f2084_1_createList_Load(x1, x2, x3, x4, x5) → f2084_1_createList_Load(x2, x4, x5)
Cond_f1909_0_createList_GT3(x1, x2, x3, x4, x5) → Cond_f1909_0_createList_GT3(x1, x3, x4, x5)

Filtered duplicate terms:

f2496_1_createList_Load(x1, x2, x3, x4) → f2496_1_createList_Load(x1, x2, x4)
f1909_0_createList_GT(x1, x2, x3) → f1909_0_createList_GT(x3)
Cond_f1909_0_createList_GT(x1, x2, x3, x4, x5) → Cond_f1909_0_createList_GT(x1, x4, x5)
Cond_f1909_0_createList_GT1(x1, x2, x3, x4) → Cond_f1909_0_createList_GT1(x1, x4)
Cond_f1909_0_createList_GT2(x1, x2, x3, x4) → Cond_f1909_0_createList_GT2(x1, x4)
f2084_1_createList_Load(x1, x2, x3) → f2084_1_createList_Load(x3)
Cond_f1909_0_createList_GT3(x1, x2, x3, x4) → Cond_f1909_0_createList_GT3(x1, x4)

Filtered unneeded terms:

Cond_f1909_0_createList_GT(x1, x2, x3) → Cond_f1909_0_createList_GT(x1, x2)
Cond_f1909_0_createList_GT2(x1, x2) → Cond_f1909_0_createList_GT2(x1)
f2475_0_createList_InvokeMethod(x1, x2, x3) → f2475_0_createList_InvokeMethod(x3)

Prepared 6 rules for path length conversion:

P rules:
f2475_0_createList_InvokeMethod(i844) → f2496_1_createList_Load(i574, i735, i844)
f1909_0_createList_GT(x0) → f2475_0_createList_InvokeMethod(-(x0, 1)) | &&(>(+(x1, 1), 0), >(x0, 0))
f2475_0_createList_InvokeMethod(x2) → f1909_0_createList_GT(x2)
f1909_0_createList_GT(x0) → f2475_0_createList_InvokeMethod(-(x0, 1)) | >(x0, 0)
f1909_0_createList_GT(x0) → f2084_1_createList_Load(-(x0, 1)) | >(x0, 0)
f1909_0_createList_GT(x0) → f1909_0_createList_GT(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 4 rules.

P rules:
f1909_0_createList_GT(x3) → f2475_0_createList_InvokeMethod(-(x3, 1)) | &&(>(x3, 0), >(x4, -1))
f2475_0_createList_InvokeMethod(x5) → f1909_0_createList_GT(x5)
f1909_0_createList_GT(x6) → f2475_0_createList_InvokeMethod(-(x6, 1)) | >(x6, 0)
f1909_0_createList_GT(x8) → f1909_0_createList_GT(-(x8, 1)) | >(x8, 0)

(18) Obligation:

Rules:
f1909_0_createList_GT(x3) → f2475_0_createList_InvokeMethod(-(x3, 1)) | &&(>(x3, 0), >(x4, -1))
f2475_0_createList_InvokeMethod(x5) → f1909_0_createList_GT(x5)
f1909_0_createList_GT(x6) → f2475_0_createList_InvokeMethod(-(x6, 1)) | >(x6, 0)
f1909_0_createList_GT(x8) → f1909_0_createList_GT(-(x8, 1)) | >(x8, 0)

(19) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f1909_0_createList_GT(x6)] = -1 + x6
[f2475_0_createList_InvokeMethod(x9)] = -1 + x9

Therefore the following rule(s) have been dropped:

f1909_0_createList_GT(x0) → f2475_0_createList_InvokeMethod(-(x0, 1)) | &&(>(x0, 0), >(x1, -1))
f1909_0_createList_GT(x3) → f2475_0_createList_InvokeMethod(-(x3, 1)) | >(x3, 0)
f1909_0_createList_GT(x4) → f1909_0_createList_GT(-(x4, 1)) | >(x4, 0)

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) IDPNonInfProof (SOUND transformation)

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIntTRSProof (SOUND transformation)

(18) Obligation:

(19) PolynomialOrderProcessor (SOUND transformation)

(20) Obligation:

(21) TerminationGraphProcessor (EQUIVALENT transformation)

(22) YES