Termination proof of /tmp/tmpLD97Al/Test3.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 2099 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 536 ms)

        ↳7 intTRS

        ↳8 LinearRankingProcessor (⇔, 1074 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 5 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 666 ms)

        ↳17 intTRS

        ↳18 LinearRankingProcessor (⇔, 66 ms)

        ↳19 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Test3 {
    public static void main(String[] args) {
	List l1 = List.mk(args.length);
	List l2 = List.mk(args.length);
	List l3 = (args.length % 2 == 0) ?
	    List.mk(args.length * args.length) : l2;

	while (length(l1) + length(l2) + length(l3) * 5 > 0)
	    if (length(l1) % 2 == 1)
		l1 = l1.getTail();
	    else if (length(l2) > length(l3))
		l2 = l2.getTail();
	    else if (l3 == null)
		break;
	    else {
		l1 = new List(new Object(), l1);
		l2 = new List(new Object(), l2);
		l3 = l3.getTail();
	    }
    }

    private static int length(List list) {
	int len = 0;

	while (list != null) {
	    list = list.getTail();
	    len++;
	}

	return len;
    }
}


public class List {
    public Object head;
    private List tail;

    public List(Object head, List tail) {
	this.head = head;
	this.tail = tail;
    }

    public List getTail() {
	return tail;
    }

    public static List mk(int len) {
	List result = null;

	while (len-- > 0)
	    result = new List(new Object(), result);

	return result;
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Test3.main([Ljava/lang/String;)V: Graph of 261 nodes with 1 SCC.

List.mk(I)LList;: Graph of 33 nodes with 1 SCC.

Test3.length(LList;)I: Graph of 77 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test3.length(LList;)I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 76 IRules

P rules:
f7048_0_length_NULL(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7054_0_length_NULL(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7054_0_length_NULL(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7062_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub))
f7062_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub)) → f7070_0_length_InvokeMethod(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub))
f7070_0_length_InvokeMethod(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub)) → f7079_0_getTail_Load(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7079_0_getTail_Load(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7192_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7192_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7213_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7192_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(o6082sub), o5981, o5982, o5983, java.lang.Object(o6082sub), java.lang.Object(o6082sub)) → f7214_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(o6082sub), o5981, o5982, o5983, java.lang.Object(o6082sub), java.lang.Object(o6082sub))
f7213_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7233_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7213_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub)) → f7234_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub))
f7233_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7266_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7233_0_getTail_FieldAccess(EOS, o5979, o5980, java.lang.Object(o6100sub), o5982, o5983, java.lang.Object(o6100sub), java.lang.Object(o6100sub)) → f7267_0_getTail_FieldAccess(EOS, o5979, o5980, java.lang.Object(o6100sub), o5982, o5983, java.lang.Object(o6100sub), java.lang.Object(o6100sub))
f7266_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7304_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7266_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, java.lang.Object(o6116sub), o5983, java.lang.Object(o6116sub), java.lang.Object(o6116sub)) → f7305_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, java.lang.Object(o6116sub), o5983, java.lang.Object(o6116sub), java.lang.Object(o6116sub))
f7304_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub)) → f7344_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(o6004sub), java.lang.Object(o6004sub))
f7304_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, java.lang.Object(o6143sub), java.lang.Object(o6143sub), java.lang.Object(o6143sub)) → f7345_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, java.lang.Object(o6143sub), java.lang.Object(o6143sub), java.lang.Object(o6143sub))
f7344_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6196)), java.lang.Object(List(EOC, o6196))) → f7400_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6196)), java.lang.Object(List(EOC, o6196)))
f7400_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6196)), java.lang.Object(List(EOC, o6196))) → f7507_0_getTail_Return(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6196)), o6196)
f7507_0_getTail_Return(EOS, o5979, o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6196)), o6196) → f7651_0_length_Store(EOS, o5979, o5980, o5981, o5982, o5983, o6196)
f7651_0_length_Store(EOS, o5979, o5980, o5981, o5982, o5983, o6196) → f7670_0_length_Inc(EOS, o5979, o5980, o5981, o5982, o5983, o6196)
f7670_0_length_Inc(EOS, o5979, o5980, o5981, o5982, o5983, o6196) → f7691_0_length_JMP(EOS, o5979, o5980, o5981, o5982, o5983, o6196)
f7691_0_length_JMP(EOS, o5979, o5980, o5981, o5982, o5983, o6196) → f7723_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, o6196)
f7723_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, o6196) → f7035_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, o6196)
f7035_0_length_Load(EOS, o5979, o5980, o5981, o5982, o5983, o5984) → f7048_0_length_NULL(EOS, o5979, o5980, o5981, o5982, o5983, o5984, o5984)
f7345_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199))) → f7404_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)))
f7404_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199))) → f7525_0_getTail_Return(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)), o6199)
f7525_0_getTail_Return(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), java.lang.Object(List(EOC, o6199)), o6199) → f7655_0_length_Store(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199)
f7655_0_length_Store(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199) → f7675_0_length_Inc(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199)
f7675_0_length_Inc(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199) → f7696_0_length_JMP(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199)
f7696_0_length_JMP(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199) → f7734_0_length_Load(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199)
f7734_0_length_Load(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199) → f7035_0_length_Load(EOS, o5979, o5980, o5981, o5982, java.lang.Object(List(EOC, o6199)), o6199)
f7305_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, java.lang.Object(List(EOC, o6150)), java.lang.Object(List(EOC, o6150))) → f7352_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, java.lang.Object(List(EOC, o6150)), java.lang.Object(List(EOC, o6150)))
f7352_0_getTail_FieldAccess(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, java.lang.Object(List(EOC, o6150)), java.lang.Object(List(EOC, o6150))) → f7411_0_getTail_Return(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, java.lang.Object(List(EOC, o6150)), o6150)
f7411_0_getTail_Return(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, java.lang.Object(List(EOC, o6150)), o6150) → f7537_0_length_Store(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, o6150)
f7537_0_length_Store(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, o6150) → f7651_0_length_Store(EOS, o5979, o5980, o5981, java.lang.Object(List(EOC, o6150)), o5983, o6150)
f7267_0_getTail_FieldAccess(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, java.lang.Object(List(EOC, o6119)), java.lang.Object(List(EOC, o6119))) → f7309_0_getTail_FieldAccess(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, java.lang.Object(List(EOC, o6119)), java.lang.Object(List(EOC, o6119)))
f7309_0_getTail_FieldAccess(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, java.lang.Object(List(EOC, o6119)), java.lang.Object(List(EOC, o6119))) → f7361_0_getTail_Return(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, java.lang.Object(List(EOC, o6119)), o6119)
f7361_0_getTail_Return(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, java.lang.Object(List(EOC, o6119)), o6119) → f7421_0_length_Store(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, o6119)
f7421_0_length_Store(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, o6119) → f7651_0_length_Store(EOS, o5979, o5980, java.lang.Object(List(EOC, o6119)), o5982, o5983, o6119)
f7234_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub)) → f7281_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub))
f7234_0_getTail_FieldAccess(EOS, java.lang.Object(o6107sub), o5980, java.lang.Object(o6107sub), o5982, o5983, java.lang.Object(o6107sub), java.lang.Object(o6107sub)) → f7282_0_getTail_FieldAccess(EOS, java.lang.Object(o6107sub), o5980, java.lang.Object(o6107sub), o5982, o5983, java.lang.Object(o6107sub), java.lang.Object(o6107sub))
f7281_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub)) → f7319_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub))
f7281_0_getTail_FieldAccess(EOS, java.lang.Object(o6122sub), o5980, o5981, java.lang.Object(o6122sub), o5983, java.lang.Object(o6122sub), java.lang.Object(o6122sub)) → f7320_0_getTail_FieldAccess(EOS, java.lang.Object(o6122sub), o5980, o5981, java.lang.Object(o6122sub), o5983, java.lang.Object(o6122sub), java.lang.Object(o6122sub))
f7319_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub)) → f7370_0_getTail_FieldAccess(EOS, java.lang.Object(o6089sub), o5980, o5981, o5982, o5983, java.lang.Object(o6089sub), java.lang.Object(o6089sub))
f7319_0_getTail_FieldAccess(EOS, java.lang.Object(o6171sub), o5980, o5981, o5982, java.lang.Object(o6171sub), java.lang.Object(o6171sub), java.lang.Object(o6171sub)) → f7371_0_getTail_FieldAccess(EOS, java.lang.Object(o6171sub), o5980, o5981, o5982, java.lang.Object(o6171sub), java.lang.Object(o6171sub), java.lang.Object(o6171sub))
f7370_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6245)), java.lang.Object(List(EOC, o6245))) → f7438_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6245)), java.lang.Object(List(EOC, o6245)))
f7438_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6245)), java.lang.Object(List(EOC, o6245))) → f7577_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6245)), o6245)
f7577_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, java.lang.Object(List(EOC, o6245)), o6245) → f7662_0_length_Store(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245)
f7662_0_length_Store(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245) → f7683_0_length_Inc(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245)
f7683_0_length_Inc(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245) → f7703_0_length_JMP(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245)
f7703_0_length_JMP(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245) → f7749_0_length_Load(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245)
f7749_0_length_Load(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245) → f7035_0_length_Load(EOS, java.lang.Object(List(EOC, o6245)), o5980, o5981, o5982, o5983, o6245)
f7371_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252))) → f7445_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)))
f7445_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252))) → f7590_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)), o6252)
f7590_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), java.lang.Object(List(EOC, o6252)), o6252) → f7668_0_length_Store(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252)
f7668_0_length_Store(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252) → f7689_0_length_Inc(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252)
f7689_0_length_Inc(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252) → f7710_0_length_JMP(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252)
f7710_0_length_JMP(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252) → f7761_0_length_Load(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252)
f7761_0_length_Load(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252) → f7035_0_length_Load(EOS, java.lang.Object(List(EOC, o6252)), o5980, o5981, o5982, java.lang.Object(List(EOC, o6252)), o6252)
f7320_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, java.lang.Object(List(EOC, o6178)), java.lang.Object(List(EOC, o6178))) → f7376_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, java.lang.Object(List(EOC, o6178)), java.lang.Object(List(EOC, o6178)))
f7376_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, java.lang.Object(List(EOC, o6178)), java.lang.Object(List(EOC, o6178))) → f7456_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, java.lang.Object(List(EOC, o6178)), o6178)
f7456_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, java.lang.Object(List(EOC, o6178)), o6178) → f7597_0_length_Store(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, o6178)
f7597_0_length_Store(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, o6178) → f7651_0_length_Store(EOS, java.lang.Object(List(EOC, o6178)), o5980, o5981, java.lang.Object(List(EOC, o6178)), o5983, o6178)
f7282_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, java.lang.Object(List(EOC, o6125)), java.lang.Object(List(EOC, o6125))) → f7321_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, java.lang.Object(List(EOC, o6125)), java.lang.Object(List(EOC, o6125)))
f7321_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, java.lang.Object(List(EOC, o6125)), java.lang.Object(List(EOC, o6125))) → f7385_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, java.lang.Object(List(EOC, o6125)), o6125)
f7385_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, java.lang.Object(List(EOC, o6125)), o6125) → f7468_0_length_Store(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, o6125)
f7468_0_length_Store(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, o6125) → f7651_0_length_Store(EOS, java.lang.Object(List(EOC, o6125)), o5980, java.lang.Object(List(EOC, o6125)), o5982, o5983, o6125)
f7214_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(o6082sub), o5981, o5982, o5983, java.lang.Object(o6082sub), java.lang.Object(o6082sub)) → f7246_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(o6082sub), o5981, o5982, o5983, java.lang.Object(o6082sub), java.lang.Object(o6082sub))
f7214_0_getTail_FieldAccess(EOS, java.lang.Object(o6093sub), java.lang.Object(o6093sub), o5981, o5982, o5983, java.lang.Object(o6093sub), java.lang.Object(o6093sub)) → f7247_0_getTail_FieldAccess(EOS, java.lang.Object(o6093sub), java.lang.Object(o6093sub), o5981, o5982, o5983, java.lang.Object(o6093sub), java.lang.Object(o6093sub))
f7246_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6110)), java.lang.Object(List(EOC, o6110))) → f7288_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6110)), java.lang.Object(List(EOC, o6110)))
f7288_0_getTail_FieldAccess(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6110)), java.lang.Object(List(EOC, o6110))) → f7328_0_getTail_Return(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6110)), o6110)
f7328_0_getTail_Return(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6110)), o6110) → f7389_0_length_Store(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, o6110)
f7389_0_length_Store(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, o6110) → f7651_0_length_Store(EOS, o5979, java.lang.Object(List(EOC, o6110)), o5981, o5982, o5983, o6110)
f7247_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113))) → f7292_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)))
f7292_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113))) → f7332_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6113)), o6113)
f7332_0_getTail_Return(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, java.lang.Object(List(EOC, o6113)), o6113) → f7393_0_length_Store(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, o6113)
f7393_0_length_Store(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, o6113) → f7651_0_length_Store(EOS, java.lang.Object(List(EOC, o6113)), java.lang.Object(List(EOC, o6113)), o5981, o5982, o5983, o6113)

Combined rules. Obtained 10 IRules

P rules:
f7048_0_length_NULL(EOS, x0, x1, x2, x3, x4, java.lang.Object(List(EOC, x5)), java.lang.Object(List(EOC, x5))) → f7048_0_length_NULL(EOS, x0, x1, x2, x3, x4, x5, x5)
f7048_0_length_NULL(EOS, x0, x1, x2, x3, java.lang.Object(List(EOC, x4)), java.lang.Object(List(EOC, x4)), java.lang.Object(List(EOC, x4))) → f7048_0_length_NULL(EOS, x0, x1, x2, x3, java.lang.Object(List(EOC, x4)), x4, x4)
f7048_0_length_NULL(EOS, x0, x1, x2, java.lang.Object(List(EOC, x3)), x4, java.lang.Object(List(EOC, x3)), java.lang.Object(List(EOC, x3))) → f7048_0_length_NULL(EOS, x0, x1, x2, java.lang.Object(List(EOC, x3)), x4, x3, x3)
f7048_0_length_NULL(EOS, x0, x1, java.lang.Object(List(EOC, x2)), x3, x4, java.lang.Object(List(EOC, x2)), java.lang.Object(List(EOC, x2))) → f7048_0_length_NULL(EOS, x0, x1, java.lang.Object(List(EOC, x2)), x3, x4, x2, x2)
f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, x3, x4, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, x3, x4, x0, x0)
f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, x3, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, x3, java.lang.Object(List(EOC, x0)), x0, x0)
f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0)), x3, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0)), x3, x0, x0)
f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, java.lang.Object(List(EOC, x0)), x2, x3, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x1, java.lang.Object(List(EOC, x0)), x2, x3, x0, x0)
f7048_0_length_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), x2, x3, x4, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x1))) → f7048_0_length_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), x2, x3, x4, x1, x1)
f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), x1, x2, x3, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f7048_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), x1, x2, x3, x0, x0)

Filtered ground terms:

f7048_0_length_NULL(x1, x2, x3, x4, x5, x6, x7, x8) → f7048_0_length_NULL(x2, x3, x4, x5, x6, x7, x8)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f7048_0_length_NULL(x1, x2, x3, x4, x5, x6, x7) → f7048_0_length_NULL(x1, x2, x3, x4, x5, x7)

Prepared 10 rules for path length conversion:

P rules:
f7048_0_length_NULL(x0, x1, x2, x3, x4, java.lang.Object(List(x5))) → f7048_0_length_NULL(x0, x1, x2, x3, x4, x5)
f7048_0_length_NULL(x0, x1, x2, x3, java.lang.Object(List(x4)), java.lang.Object(List(x4))) → f7048_0_length_NULL(x0, x1, x2, x3, java.lang.Object(List(x4)), x4)
f7048_0_length_NULL(x0, x1, x2, java.lang.Object(List(x3)), x4, java.lang.Object(List(x3))) → f7048_0_length_NULL(x0, x1, x2, java.lang.Object(List(x3)), x4, x3)
f7048_0_length_NULL(x0, x1, java.lang.Object(List(x2)), x3, x4, java.lang.Object(List(x2))) → f7048_0_length_NULL(x0, x1, java.lang.Object(List(x2)), x3, x4, x2)
f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, x3, x4, java.lang.Object(List(x0))) → f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, x3, x4, x0)
f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, x3, java.lang.Object(List(x0)), java.lang.Object(List(x0))) → f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, x3, java.lang.Object(List(x0)), x0)
f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, java.lang.Object(List(x0)), x3, java.lang.Object(List(x0))) → f7048_0_length_NULL(java.lang.Object(List(x0)), x1, x2, java.lang.Object(List(x0)), x3, x0)
f7048_0_length_NULL(java.lang.Object(List(x0)), x1, java.lang.Object(List(x0)), x2, x3, java.lang.Object(List(x0))) → f7048_0_length_NULL(java.lang.Object(List(x0)), x1, java.lang.Object(List(x0)), x2, x3, x0)
f7048_0_length_NULL(x0, java.lang.Object(List(x1)), x2, x3, x4, java.lang.Object(List(x1))) → f7048_0_length_NULL(x0, java.lang.Object(List(x1)), x2, x3, x4, x1)
f7048_0_length_NULL(java.lang.Object(List(x0)), java.lang.Object(List(x0)), x1, x2, x3, java.lang.Object(List(x0))) → f7048_0_length_NULL(java.lang.Object(List(x0)), java.lang.Object(List(x0)), x1, x2, x3, x0)

Finished conversion. Obtained 10 rules.

P rules:
f7048_0_length_NULL(v53, v54, v55, v56, v57, v58) → f7048_0_length_NULL(v59, v60, v61, v62, v63, v64) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v64, 1), 0), <=(+(v64, 1), v58)), >(+(v63, 1), 0)), <=(v63, v57)), >(+(v62, 1), 0)), <=(v62, v56)), >(+(v61, 1), 0)), <=(v61, v55)), >(+(v60, 1), 0)), <=(v60, v54)), >(+(v59, 1), 0)), <=(v59, v53)), >(+(v58, 1), 1)), >(+(v57, 1), 0)), >(+(v56, 1), 0)), >(+(v55, 1), 0)), >(+(v54, 1), 0)), >(+(v53, 1), 0))
f7048_0_length_NULL(v65, v66, v67, v68, v69, v70) → f7048_0_length_NULL(v71, v72, v73, v74, v75, v76) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v76, 1), 0), <=(+(v76, 1), v70)), <=(+(v76, 1), v69)), >(+(v75, 1), 1)), <=(v75, v70)), <=(v75, v69)), >(+(v74, 1), 0)), <=(v74, v68)), >(+(v73, 1), 0)), <=(v73, v67)), >(+(v72, 1), 0)), <=(v72, v66)), >(+(v71, 1), 0)), <=(v71, v65)), >(+(v70, 1), 1)), >(+(v69, 1), 1)), >(+(v68, 1), 0)), >(+(v67, 1), 0)), >(+(v66, 1), 0)), >(+(v65, 1), 0))
f7048_0_length_NULL(v77, v78, v79, v80, v81, v82) → f7048_0_length_NULL(v83, v84, v85, v86, v87, v88) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v88, 1), 0), <=(+(v88, 1), v82)), <=(+(v88, 1), v80)), >(+(v87, 1), 0)), <=(v87, v81)), >(+(v86, 1), 1)), <=(v86, v82)), <=(v86, v80)), >(+(v85, 1), 0)), <=(v85, v79)), >(+(v84, 1), 0)), <=(v84, v78)), >(+(v83, 1), 0)), <=(v83, v77)), >(+(v82, 1), 1)), >(+(v81, 1), 0)), >(+(v80, 1), 1)), >(+(v79, 1), 0)), >(+(v78, 1), 0)), >(+(v77, 1), 0))
f7048_0_length_NULL(v89, v90, v91, v92, v93, v94) → f7048_0_length_NULL(v95, v96, v97, v98, v99, v100) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v99, 1), 0), <=(v99, v93)), >(+(v98, 1), 0)), <=(v98, v92)), >(+(v97, 1), 1)), <=(v97, v94)), <=(v97, v91)), >(+(v96, 1), 0)), <=(v96, v90)), >(+(v95, 1), 0)), <=(v95, v89)), >=(v94, +(v100, 1))), >(+(v94, 1), 1)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >=(v91, +(v100, 1))), >(+(v91, 1), 1)), >(+(v90, 1), 0)), >(+(v89, 1), 0)), >(+(v100, 1), 0))
f7048_0_length_NULL(v101, v102, v103, v104, v105, v106) → f7048_0_length_NULL(v107, v108, v109, v110, v111, v112) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v112, 1), 0), <=(+(v112, 1), v106)), <=(+(v112, 1), v101)), >(+(v111, 1), 0)), <=(v111, v105)), >(+(v110, 1), 0)), <=(v110, v104)), >(+(v109, 1), 0)), <=(v109, v103)), >(+(v108, 1), 0)), <=(v108, v102)), >(+(v107, 1), 1)), <=(v107, v106)), <=(v107, v101)), >(+(v106, 1), 1)), >(+(v105, 1), 0)), >(+(v104, 1), 0)), >(+(v103, 1), 0)), >(+(v102, 1), 0)), >(+(v101, 1), 1))
f7048_0_length_NULL(v113, v114, v115, v116, v117, v118) → f7048_0_length_NULL(v119, v120, v121, v122, v123, v124) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v124, 1), 0), <=(+(v124, 1), v118)), <=(+(v124, 1), v117)), <=(+(v124, 1), v113)), >(+(v123, 1), 1)), <=(v123, v118)), <=(v123, v117)), <=(v123, v113)), >(+(v122, 1), 0)), <=(v122, v116)), >(+(v121, 1), 0)), <=(v121, v115)), >(+(v120, 1), 0)), <=(v120, v114)), >(+(v119, 1), 1)), <=(v119, v118)), <=(v119, v117)), <=(v119, v113)), >(+(v118, 1), 1)), >(+(v117, 1), 1)), >(+(v116, 1), 0)), >(+(v115, 1), 0)), >(+(v114, 1), 0)), >(+(v113, 1), 1))
f7048_0_length_NULL(v125, v126, v127, v128, v129, v130) → f7048_0_length_NULL(v131, v132, v133, v134, v135, v136) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v136, 1), 0), <=(+(v136, 1), v130)), <=(+(v136, 1), v128)), <=(+(v136, 1), v125)), >(+(v135, 1), 0)), <=(v135, v129)), >(+(v134, 1), 1)), <=(v134, v130)), <=(v134, v128)), <=(v134, v125)), >(+(v133, 1), 0)), <=(v133, v127)), >(+(v132, 1), 0)), <=(v132, v126)), >(+(v131, 1), 1)), <=(v131, v130)), <=(v131, v128)), <=(v131, v125)), >(+(v130, 1), 1)), >(+(v129, 1), 0)), >(+(v128, 1), 1)), >(+(v127, 1), 0)), >(+(v126, 1), 0)), >(+(v125, 1), 1))
f7048_0_length_NULL(v137, v138, v139, v140, v141, v142) → f7048_0_length_NULL(v143, v144, v145, v146, v147, v148) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v148, 1), 0), <=(+(v148, 1), v142)), <=(+(v148, 1), v139)), <=(+(v148, 1), v137)), >(+(v147, 1), 0)), <=(v147, v141)), >(+(v146, 1), 0)), <=(v146, v140)), >(+(v145, 1), 1)), <=(v145, v142)), <=(v145, v139)), <=(v145, v137)), >(+(v144, 1), 0)), <=(v144, v138)), >(+(v143, 1), 1)), <=(v143, v142)), <=(v143, v139)), <=(v143, v137)), >(+(v142, 1), 1)), >(+(v141, 1), 0)), >(+(v140, 1), 0)), >(+(v139, 1), 1)), >(+(v138, 1), 0)), >(+(v137, 1), 1))
f7048_0_length_NULL(v149, v150, v151, v152, v153, v154) → f7048_0_length_NULL(v155, v156, v157, v158, v159, v160) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v160, 1), 0), <=(+(v160, 1), v154)), <=(+(v160, 1), v150)), >(+(v159, 1), 0)), <=(v159, v153)), >(+(v158, 1), 0)), <=(v158, v152)), >(+(v157, 1), 0)), <=(v157, v151)), >(+(v156, 1), 1)), <=(v156, v154)), <=(v156, v150)), >(+(v155, 1), 0)), <=(v155, v149)), >(+(v154, 1), 1)), >(+(v153, 1), 0)), >(+(v152, 1), 0)), >(+(v151, 1), 0)), >(+(v150, 1), 1)), >(+(v149, 1), 0))
f7048_0_length_NULL(v161, v162, v163, v164, v165, v166) → f7048_0_length_NULL(v167, v168, v169, v170, v171, v172) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v172, 1), 0), <=(+(v172, 1), v166)), <=(+(v172, 1), v162)), <=(+(v172, 1), v161)), >(+(v171, 1), 0)), <=(v171, v165)), >(+(v170, 1), 0)), <=(v170, v164)), >(+(v169, 1), 0)), <=(v169, v163)), >(+(v168, 1), 1)), <=(v168, v166)), <=(v168, v162)), <=(v168, v161)), >(+(v167, 1), 1)), <=(v167, v166)), <=(v167, v162)), <=(v167, v161)), >(+(v166, 1), 1)), >(+(v165, 1), 0)), >(+(v164, 1), 0)), >(+(v163, 1), 0)), >(+(v162, 1), 1)), >(+(v161, 1), 1))

(7) Obligation:

Rules:
f7048_0_length_NULL(v53, v54, v55, v56, v57, v58) → f7048_0_length_NULL(v59, v60, v61, v62, v63, v64) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v64, 1), 0), <=(+(v64, 1), v58)), >(+(v63, 1), 0)), <=(v63, v57)), >(+(v62, 1), 0)), <=(v62, v56)), >(+(v61, 1), 0)), <=(v61, v55)), >(+(v60, 1), 0)), <=(v60, v54)), >(+(v59, 1), 0)), <=(v59, v53)), >(+(v58, 1), 1)), >(+(v57, 1), 0)), >(+(v56, 1), 0)), >(+(v55, 1), 0)), >(+(v54, 1), 0)), >(+(v53, 1), 0))
f7048_0_length_NULL(v65, v66, v67, v68, v69, v70) → f7048_0_length_NULL(v71, v72, v73, v74, v75, v76) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v76, 1), 0), <=(+(v76, 1), v70)), <=(+(v76, 1), v69)), >(+(v75, 1), 1)), <=(v75, v70)), <=(v75, v69)), >(+(v74, 1), 0)), <=(v74, v68)), >(+(v73, 1), 0)), <=(v73, v67)), >(+(v72, 1), 0)), <=(v72, v66)), >(+(v71, 1), 0)), <=(v71, v65)), >(+(v70, 1), 1)), >(+(v69, 1), 1)), >(+(v68, 1), 0)), >(+(v67, 1), 0)), >(+(v66, 1), 0)), >(+(v65, 1), 0))
f7048_0_length_NULL(v77, v78, v79, v80, v81, v82) → f7048_0_length_NULL(v83, v84, v85, v86, v87, v88) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v88, 1), 0), <=(+(v88, 1), v82)), <=(+(v88, 1), v80)), >(+(v87, 1), 0)), <=(v87, v81)), >(+(v86, 1), 1)), <=(v86, v82)), <=(v86, v80)), >(+(v85, 1), 0)), <=(v85, v79)), >(+(v84, 1), 0)), <=(v84, v78)), >(+(v83, 1), 0)), <=(v83, v77)), >(+(v82, 1), 1)), >(+(v81, 1), 0)), >(+(v80, 1), 1)), >(+(v79, 1), 0)), >(+(v78, 1), 0)), >(+(v77, 1), 0))
f7048_0_length_NULL(v89, v90, v91, v92, v93, v94) → f7048_0_length_NULL(v95, v96, v97, v98, v99, v100) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v99, 1), 0), <=(v99, v93)), >(+(v98, 1), 0)), <=(v98, v92)), >(+(v97, 1), 1)), <=(v97, v94)), <=(v97, v91)), >(+(v96, 1), 0)), <=(v96, v90)), >(+(v95, 1), 0)), <=(v95, v89)), >=(v94, +(v100, 1))), >(+(v94, 1), 1)), >(+(v93, 1), 0)), >(+(v92, 1), 0)), >=(v91, +(v100, 1))), >(+(v91, 1), 1)), >(+(v90, 1), 0)), >(+(v89, 1), 0)), >(+(v100, 1), 0))
f7048_0_length_NULL(v101, v102, v103, v104, v105, v106) → f7048_0_length_NULL(v107, v108, v109, v110, v111, v112) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v112, 1), 0), <=(+(v112, 1), v106)), <=(+(v112, 1), v101)), >(+(v111, 1), 0)), <=(v111, v105)), >(+(v110, 1), 0)), <=(v110, v104)), >(+(v109, 1), 0)), <=(v109, v103)), >(+(v108, 1), 0)), <=(v108, v102)), >(+(v107, 1), 1)), <=(v107, v106)), <=(v107, v101)), >(+(v106, 1), 1)), >(+(v105, 1), 0)), >(+(v104, 1), 0)), >(+(v103, 1), 0)), >(+(v102, 1), 0)), >(+(v101, 1), 1))
f7048_0_length_NULL(v113, v114, v115, v116, v117, v118) → f7048_0_length_NULL(v119, v120, v121, v122, v123, v124) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v124, 1), 0), <=(+(v124, 1), v118)), <=(+(v124, 1), v117)), <=(+(v124, 1), v113)), >(+(v123, 1), 1)), <=(v123, v118)), <=(v123, v117)), <=(v123, v113)), >(+(v122, 1), 0)), <=(v122, v116)), >(+(v121, 1), 0)), <=(v121, v115)), >(+(v120, 1), 0)), <=(v120, v114)), >(+(v119, 1), 1)), <=(v119, v118)), <=(v119, v117)), <=(v119, v113)), >(+(v118, 1), 1)), >(+(v117, 1), 1)), >(+(v116, 1), 0)), >(+(v115, 1), 0)), >(+(v114, 1), 0)), >(+(v113, 1), 1))
f7048_0_length_NULL(v125, v126, v127, v128, v129, v130) → f7048_0_length_NULL(v131, v132, v133, v134, v135, v136) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v136, 1), 0), <=(+(v136, 1), v130)), <=(+(v136, 1), v128)), <=(+(v136, 1), v125)), >(+(v135, 1), 0)), <=(v135, v129)), >(+(v134, 1), 1)), <=(v134, v130)), <=(v134, v128)), <=(v134, v125)), >(+(v133, 1), 0)), <=(v133, v127)), >(+(v132, 1), 0)), <=(v132, v126)), >(+(v131, 1), 1)), <=(v131, v130)), <=(v131, v128)), <=(v131, v125)), >(+(v130, 1), 1)), >(+(v129, 1), 0)), >(+(v128, 1), 1)), >(+(v127, 1), 0)), >(+(v126, 1), 0)), >(+(v125, 1), 1))
f7048_0_length_NULL(v137, v138, v139, v140, v141, v142) → f7048_0_length_NULL(v143, v144, v145, v146, v147, v148) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v148, 1), 0), <=(+(v148, 1), v142)), <=(+(v148, 1), v139)), <=(+(v148, 1), v137)), >(+(v147, 1), 0)), <=(v147, v141)), >(+(v146, 1), 0)), <=(v146, v140)), >(+(v145, 1), 1)), <=(v145, v142)), <=(v145, v139)), <=(v145, v137)), >(+(v144, 1), 0)), <=(v144, v138)), >(+(v143, 1), 1)), <=(v143, v142)), <=(v143, v139)), <=(v143, v137)), >(+(v142, 1), 1)), >(+(v141, 1), 0)), >(+(v140, 1), 0)), >(+(v139, 1), 1)), >(+(v138, 1), 0)), >(+(v137, 1), 1))
f7048_0_length_NULL(v149, v150, v151, v152, v153, v154) → f7048_0_length_NULL(v155, v156, v157, v158, v159, v160) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v160, 1), 0), <=(+(v160, 1), v154)), <=(+(v160, 1), v150)), >(+(v159, 1), 0)), <=(v159, v153)), >(+(v158, 1), 0)), <=(v158, v152)), >(+(v157, 1), 0)), <=(v157, v151)), >(+(v156, 1), 1)), <=(v156, v154)), <=(v156, v150)), >(+(v155, 1), 0)), <=(v155, v149)), >(+(v154, 1), 1)), >(+(v153, 1), 0)), >(+(v152, 1), 0)), >(+(v151, 1), 0)), >(+(v150, 1), 1)), >(+(v149, 1), 0))
f7048_0_length_NULL(v161, v162, v163, v164, v165, v166) → f7048_0_length_NULL(v167, v168, v169, v170, v171, v172) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v172, 1), 0), <=(+(v172, 1), v166)), <=(+(v172, 1), v162)), <=(+(v172, 1), v161)), >(+(v171, 1), 0)), <=(v171, v165)), >(+(v170, 1), 0)), <=(v170, v164)), >(+(v169, 1), 0)), <=(v169, v163)), >(+(v168, 1), 1)), <=(v168, v166)), <=(v168, v162)), <=(v168, v161)), >(+(v167, 1), 1)), <=(v167, v166)), <=(v167, v162)), <=(v167, v161)), >(+(v166, 1), 1)), >(+(v165, 1), 0)), >(+(v164, 1), 0)), >(+(v163, 1), 0)), >(+(v162, 1), 1)), >(+(v161, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f7048_0_length_NULL(x)] = 1·x₆

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f7048_0_length_NULL(x0, x1, x2, x3, x4, x5) → f7048_0_length_NULL(x6, x7, x8, x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 0), <=(+(x11, 1), x5)), >(+(x10, 1), 0)), <=(x10, x4)), >(+(x9, 1), 0)), <=(x9, x3)), >(+(x8, 1), 0)), <=(x8, x2)), >(+(x7, 1), 0)), <=(x7, x1)), >(+(x6, 1), 0)), <=(x6, x0)), >(+(x5, 1), 1)), >(+(x4, 1), 0)), >(+(x3, 1), 0)), >(+(x2, 1), 0)), >(+(x1, 1), 0)), >(+(x0, 1), 0))
f7048_0_length_NULL(x12, x13, x14, x15, x16, x17) → f7048_0_length_NULL(x18, x19, x20, x21, x22, x23) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x23, 1), 0), <=(+(x23, 1), x17)), <=(+(x23, 1), x16)), >(+(x22, 1), 1)), <=(x22, x17)), <=(x22, x16)), >(+(x21, 1), 0)), <=(x21, x15)), >(+(x20, 1), 0)), <=(x20, x14)), >(+(x19, 1), 0)), <=(x19, x13)), >(+(x18, 1), 0)), <=(x18, x12)), >(+(x17, 1), 1)), >(+(x16, 1), 1)), >(+(x15, 1), 0)), >(+(x14, 1), 0)), >(+(x13, 1), 0)), >(+(x12, 1), 0))
f7048_0_length_NULL(x24, x25, x26, x27, x28, x29) → f7048_0_length_NULL(x30, x31, x32, x33, x34, x35) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x35, 1), 0), <=(+(x35, 1), x29)), <=(+(x35, 1), x27)), >(+(x34, 1), 0)), <=(x34, x28)), >(+(x33, 1), 1)), <=(x33, x29)), <=(x33, x27)), >(+(x32, 1), 0)), <=(x32, x26)), >(+(x31, 1), 0)), <=(x31, x25)), >(+(x30, 1), 0)), <=(x30, x24)), >(+(x29, 1), 1)), >(+(x28, 1), 0)), >(+(x27, 1), 1)), >(+(x26, 1), 0)), >(+(x25, 1), 0)), >(+(x24, 1), 0))
f7048_0_length_NULL(x36, x37, x38, x39, x40, x41) → f7048_0_length_NULL(x42, x43, x44, x45, x46, x47) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x46, 1), 0), <=(x46, x40)), >(+(x45, 1), 0)), <=(x45, x39)), >(+(x44, 1), 1)), <=(x44, x41)), <=(x44, x38)), >(+(x43, 1), 0)), <=(x43, x37)), >(+(x42, 1), 0)), <=(x42, x36)), >=(x41, +(x47, 1))), >(+(x41, 1), 1)), >(+(x40, 1), 0)), >(+(x39, 1), 0)), >=(x38, +(x47, 1))), >(+(x38, 1), 1)), >(+(x37, 1), 0)), >(+(x36, 1), 0)), >(+(x47, 1), 0))
f7048_0_length_NULL(x48, x49, x50, x51, x52, x53) → f7048_0_length_NULL(x54, x55, x56, x57, x58, x59) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x59, 1), 0), <=(+(x59, 1), x53)), <=(+(x59, 1), x48)), >(+(x58, 1), 0)), <=(x58, x52)), >(+(x57, 1), 0)), <=(x57, x51)), >(+(x56, 1), 0)), <=(x56, x50)), >(+(x55, 1), 0)), <=(x55, x49)), >(+(x54, 1), 1)), <=(x54, x53)), <=(x54, x48)), >(+(x53, 1), 1)), >(+(x52, 1), 0)), >(+(x51, 1), 0)), >(+(x50, 1), 0)), >(+(x49, 1), 0)), >(+(x48, 1), 1))
f7048_0_length_NULL(x60, x61, x62, x63, x64, x65) → f7048_0_length_NULL(x66, x67, x68, x69, x70, x71) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x71, 1), 0), <=(+(x71, 1), x65)), <=(+(x71, 1), x64)), <=(+(x71, 1), x60)), >(+(x70, 1), 1)), <=(x70, x65)), <=(x70, x64)), <=(x70, x60)), >(+(x69, 1), 0)), <=(x69, x63)), >(+(x68, 1), 0)), <=(x68, x62)), >(+(x67, 1), 0)), <=(x67, x61)), >(+(x66, 1), 1)), <=(x66, x65)), <=(x66, x64)), <=(x66, x60)), >(+(x65, 1), 1)), >(+(x64, 1), 1)), >(+(x63, 1), 0)), >(+(x62, 1), 0)), >(+(x61, 1), 0)), >(+(x60, 1), 1))
f7048_0_length_NULL(x72, x73, x74, x75, x76, x77) → f7048_0_length_NULL(x78, x79, x80, x81, x82, x83) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x83, 1), 0), <=(+(x83, 1), x77)), <=(+(x83, 1), x75)), <=(+(x83, 1), x72)), >(+(x82, 1), 0)), <=(x82, x76)), >(+(x81, 1), 1)), <=(x81, x77)), <=(x81, x75)), <=(x81, x72)), >(+(x80, 1), 0)), <=(x80, x74)), >(+(x79, 1), 0)), <=(x79, x73)), >(+(x78, 1), 1)), <=(x78, x77)), <=(x78, x75)), <=(x78, x72)), >(+(x77, 1), 1)), >(+(x76, 1), 0)), >(+(x75, 1), 1)), >(+(x74, 1), 0)), >(+(x73, 1), 0)), >(+(x72, 1), 1))
f7048_0_length_NULL(x84, x85, x86, x87, x88, x89) → f7048_0_length_NULL(x90, x91, x92, x93, x94, x95) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x95, 1), 0), <=(+(x95, 1), x89)), <=(+(x95, 1), x86)), <=(+(x95, 1), x84)), >(+(x94, 1), 0)), <=(x94, x88)), >(+(x93, 1), 0)), <=(x93, x87)), >(+(x92, 1), 1)), <=(x92, x89)), <=(x92, x86)), <=(x92, x84)), >(+(x91, 1), 0)), <=(x91, x85)), >(+(x90, 1), 1)), <=(x90, x89)), <=(x90, x86)), <=(x90, x84)), >(+(x89, 1), 1)), >(+(x88, 1), 0)), >(+(x87, 1), 0)), >(+(x86, 1), 1)), >(+(x85, 1), 0)), >(+(x84, 1), 1))
f7048_0_length_NULL(x96, x97, x98, x99, x100, x101) → f7048_0_length_NULL(x102, x103, x104, x105, x106, x107) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x107, 1), 0), <=(+(x107, 1), x101)), <=(+(x107, 1), x97)), >(+(x106, 1), 0)), <=(x106, x100)), >(+(x105, 1), 0)), <=(x105, x99)), >(+(x104, 1), 0)), <=(x104, x98)), >(+(x103, 1), 1)), <=(x103, x101)), <=(x103, x97)), >(+(x102, 1), 0)), <=(x102, x96)), >(+(x101, 1), 1)), >(+(x100, 1), 0)), >(+(x99, 1), 0)), >(+(x98, 1), 0)), >(+(x97, 1), 1)), >(+(x96, 1), 0))
f7048_0_length_NULL(x108, x109, x110, x111, x112, x113) → f7048_0_length_NULL(x114, x115, x116, x117, x118, x119) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x119, 1), 0), <=(+(x119, 1), x113)), <=(+(x119, 1), x109)), <=(+(x119, 1), x108)), >(+(x118, 1), 0)), <=(x118, x112)), >(+(x117, 1), 0)), <=(x117, x111)), >(+(x116, 1), 0)), <=(x116, x110)), >(+(x115, 1), 1)), <=(x115, x113)), <=(x115, x109)), <=(x115, x108)), >(+(x114, 1), 1)), <=(x114, x113)), <=(x114, x109)), <=(x114, x108)), >(+(x113, 1), 1)), >(+(x112, 1), 0)), >(+(x111, 1), 0)), >(+(x110, 1), 0)), >(+(x109, 1), 1)), >(+(x108, 1), 1))

(9) YES

(10) Obligation:

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

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f848_0_mk_Inc(EOS, i121, i121) → f856_0_mk_LE(EOS, +(i121, -1), i121)
f856_0_mk_LE(EOS, i124, i129) → f862_0_mk_LE(EOS, i124, i129)
f862_0_mk_LE(EOS, i124, i129) → f886_0_mk_New(EOS, i124) | >(i129, 0)
f886_0_mk_New(EOS, i124) → f893_0_mk_Duplicate(EOS, i124)
f893_0_mk_Duplicate(EOS, i124) → f903_0_mk_New(EOS, i124)
f903_0_mk_New(EOS, i124) → f950_0_mk_Duplicate(EOS, i124)
f950_0_mk_Duplicate(EOS, i124) → f958_0_mk_InvokeMethod(EOS, i124)
f958_0_mk_InvokeMethod(EOS, i124) → f959_0_mk_Load(EOS, i124)
f959_0_mk_Load(EOS, i124) → f970_0_mk_InvokeMethod(EOS, i124)
f970_0_mk_InvokeMethod(EOS, i124) → f995_0__init__Load(EOS, i124)
f995_0__init__Load(EOS, i124) → f1010_0__init__InvokeMethod(EOS, i124)
f1010_0__init__InvokeMethod(EOS, i124) → f1014_0__init__Load(EOS, i124)
f1014_0__init__Load(EOS, i124) → f1023_0__init__Load(EOS, i124)
f1023_0__init__Load(EOS, i124) → f1031_0__init__FieldAccess(EOS, i124)
f1031_0__init__FieldAccess(EOS, i124) → f1038_0__init__Load(EOS, i124)
f1038_0__init__Load(EOS, i124) → f1044_0__init__Load(EOS, i124)
f1044_0__init__Load(EOS, i124) → f1051_0__init__FieldAccess(EOS, i124)
f1051_0__init__FieldAccess(EOS, i124) → f1059_0__init__Return(EOS, i124)
f1059_0__init__Return(EOS, i124) → f1063_0_mk_Store(EOS, i124)
f1063_0_mk_Store(EOS, i124) → f1067_0_mk_JMP(EOS, i124)
f1067_0_mk_JMP(EOS, i124) → f1082_0_mk_Load(EOS, i124)
f1082_0_mk_Load(EOS, i124) → f841_0_mk_Load(EOS, i124)
f841_0_mk_Load(EOS, i121) → f848_0_mk_Inc(EOS, i121, i121)

Combined rules. Obtained 1 IRules

P rules:
f848_0_mk_Inc(EOS, x0, x0) → f848_0_mk_Inc(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f848_0_mk_Inc(x1, x2, x3) → f848_0_mk_Inc(x2, x3)
Cond_f848_0_mk_Inc(x1, x2, x3, x4) → Cond_f848_0_mk_Inc(x1, x3, x4)

Filtered duplicate terms:

f848_0_mk_Inc(x1, x2) → f848_0_mk_Inc(x2)
Cond_f848_0_mk_Inc(x1, x2, x3) → Cond_f848_0_mk_Inc(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f848_0_mk_Inc(x0) → f848_0_mk_Inc(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f848_0_mk_Inc(x0) → f848_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(12) Obligation:

Rules:
f848_0_mk_Inc(x0) → f848_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f848_0_mk_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:

f848_0_mk_Inc(x0) → f848_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test3.main([Ljava/lang/String;)V
SCC calls the following helper methods: Test3.length(LList;)I
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 141 IRules

P rules:
f2589_0_main_InvokeMethod(EOS, o1621, o1622, o1623, o1621) → f2593_0_length_ConstantStackPush(EOS, o1621, o1621)
f2589_0_main_InvokeMethod(EOS, o1621, o1622, o1623, o1621) → f2593_1_length_ConstantStackPush(EOS, o1621, o1622, o1623, o1621, o1621)
f2593_0_length_ConstantStackPush(EOS, o1621, o1621) → f2596_0_length_ConstantStackPush(EOS, o1621, o1621)
f7136_0_length_Return(EOS, o6019, o1622, o1623, o6019, i669) → f3565_0_length_Return(EOS, o6019, o1622, o1623, o6019, i669)
f3565_0_length_Return(EOS, o2727, o2728, o2729, o2727, i418) → f3616_0_main_Load(EOS, o2727, o2728, o2729, i418)
f3616_0_main_Load(EOS, o2727, o2728, o2729, i418) → f3619_0_main_InvokeMethod(EOS, o2727, o2728, o2729, i418, o2728)
f3619_0_main_InvokeMethod(EOS, o2727, o2728, o2729, i418, o2728) → f3632_0_length_ConstantStackPush(EOS, o2728, o2729, o2728)
f3619_0_main_InvokeMethod(EOS, o2727, o2728, o2729, i418, o2728) → f3632_1_length_ConstantStackPush(EOS, o2727, o2728, o2729, i418, o2728, o2728)
f3632_0_length_ConstantStackPush(EOS, o2728, o2729, o2728) → f3636_0_length_ConstantStackPush(EOS, o2728, o2729, o2728)
f7173_0_length_Return(EOS, o2727, o6028, o6030, i418, o6028, i670) → f3969_0_length_Return(EOS, o2727, o6028, o6030, i418, o6028, i670)
f3969_0_length_Return(EOS, o3180, o3181, o3182, i418, o3181, i482) → f4004_0_main_IntArithmetic(EOS, o3180, o3181, o3182, i418, i482)
f4004_0_main_IntArithmetic(EOS, o3180, o3181, o3182, i418, i482) → f4015_0_main_Load(EOS, o3180, o3181, o3182, +(i418, i482)) | &&(>=(i418, 0), >=(i482, 0))
f4015_0_main_Load(EOS, o3180, o3181, o3182, i484) → f4019_0_main_InvokeMethod(EOS, o3180, o3181, o3182, i484, o3182)
f4019_0_main_InvokeMethod(EOS, o3180, o3181, o3182, i484, o3182) → f4022_0_length_ConstantStackPush(EOS, o3182, o3181, o3182)
f4019_0_main_InvokeMethod(EOS, o3180, o3181, o3182, i484, o3182) → f4022_1_length_ConstantStackPush(EOS, o3180, o3181, o3182, i484, o3182, o3182)
f4022_0_length_ConstantStackPush(EOS, o3182, o3181, o3182) → f4031_0_length_ConstantStackPush(EOS, o3182, o3181, o3182)
f7198_0_length_Return(EOS, o3180, o6038, o6040, i484, o6040, i671) → f4063_0_length_Return(EOS, o3180, o6038, o6040, i484, o6040, i671)
f4063_0_length_Return(EOS, o3180, o3252, o3254, i484, o3254, i485) → f4067_0_main_ConstantStackPush(EOS, o3180, o3252, o3254, i484, i485)
f4067_0_main_ConstantStackPush(EOS, o3180, o3252, o3254, i484, i485) → f4071_0_main_IntArithmetic(EOS, o3180, o3252, o3254, i484, i485, 5)
f4071_0_main_IntArithmetic(EOS, o3180, o3252, o3254, i484, i485, matching1) → f4074_0_main_IntArithmetic(EOS, o3180, o3252, o3254, i484, *(i485, 5)) | =(matching1, 5)
f4074_0_main_IntArithmetic(EOS, o3180, o3252, o3254, i484, i486) → f4079_0_main_LE(EOS, o3180, o3252, o3254, +(i484, i486)) | &&(>=(i484, 0), >=(i486, 0))
f4079_0_main_LE(EOS, o3180, o3252, o3254, i489) → f4083_0_main_LE(EOS, o3180, o3252, o3254, i489)
f4083_0_main_LE(EOS, o3180, o3252, o3254, i489) → f4098_0_main_Load(EOS, o3180, o3252, o3254) | >(i489, 0)
f4098_0_main_Load(EOS, o3180, o3252, o3254) → f4107_0_main_InvokeMethod(EOS, o3180, o3252, o3254, o3180)
f4107_0_main_InvokeMethod(EOS, o3180, o3252, o3254, o3180) → f4116_0_length_ConstantStackPush(EOS, o3180, o3180)
f4107_0_main_InvokeMethod(EOS, o3180, o3252, o3254, o3180) → f4116_1_length_ConstantStackPush(EOS, o3180, o3252, o3254, o3180, o3180)
f4116_0_length_ConstantStackPush(EOS, o3180, o3180) → f4123_0_length_ConstantStackPush(EOS, o3180, o3180)
f7221_0_length_Return(EOS, o6048, o3252, o3254, o6048, i673) → f4163_0_length_Return(EOS, o6048, o3252, o3254, o6048, i673)
f4163_0_length_Return(EOS, o3461, o3252, o3254, o3461, i490) → f4165_0_main_ConstantStackPush(EOS, o3461, o3252, o3254, i490)
f4165_0_main_ConstantStackPush(EOS, o3461, o3252, o3254, i490) → f4167_0_main_IntArithmetic(EOS, o3461, o3252, o3254, i490, 2)
f4167_0_main_IntArithmetic(EOS, o3461, o3252, o3254, i490, matching1) → f4172_0_main_ConstantStackPush(EOS, o3461, o3252, o3254, %(i490, 2)) | =(matching1, 2)
f4172_0_main_ConstantStackPush(EOS, o3461, o3252, o3254, i491) → f4177_0_main_NE(EOS, o3461, o3252, o3254, i491, 1)
f4177_0_main_NE(EOS, o3461, o3252, o3254, matching1, matching2) → f4180_0_main_NE(EOS, o3461, o3252, o3254, 0, 1) | &&(&&(=(i491, 0), =(matching1, 0)), =(matching2, 1))
f4177_0_main_NE(EOS, o3461, o3252, o3254, matching1, matching2) → f4181_0_main_NE(EOS, o3461, o3252, o3254, 1, 1) | &&(&&(=(i491, 1), =(matching1, 1)), =(matching2, 1))
f4180_0_main_NE(EOS, o3461, o3252, o3254, matching1, matching2) → f4182_0_main_Load(EOS, o3461, o3252, o3254) | &&(=(matching1, 0), =(matching2, 1))
f4182_0_main_Load(EOS, o3461, o3252, o3254) → f4191_0_main_InvokeMethod(EOS, o3461, o3252, o3254, o3252)
f4191_0_main_InvokeMethod(EOS, o3461, o3252, o3254, o3252) → f4205_0_length_ConstantStackPush(EOS, o3252, o3254, o3252)
f4191_0_main_InvokeMethod(EOS, o3461, o3252, o3254, o3252) → f4205_1_length_ConstantStackPush(EOS, o3461, o3252, o3254, o3252, o3252)
f4205_0_length_ConstantStackPush(EOS, o3252, o3254, o3252) → f4216_0_length_ConstantStackPush(EOS, o3252, o3254, o3252)
f7252_0_length_Return(EOS, o3461, o6057, o6059, o6057, i674) → f4290_0_length_Return(EOS, o3461, o6057, o6059, o6057, i674)
f4290_0_length_Return(EOS, o3461, o3576, o3578, o3576, i500) → f4294_0_main_Load(EOS, o3461, o3576, o3578, i500)
f4294_0_main_Load(EOS, o3461, o3576, o3578, i500) → f4298_0_main_InvokeMethod(EOS, o3461, o3576, o3578, i500, o3578)
f4298_0_main_InvokeMethod(EOS, o3461, o3576, o3578, i500, o3578) → f4306_0_length_ConstantStackPush(EOS, o3578, o3576, o3578)
f4298_0_main_InvokeMethod(EOS, o3461, o3576, o3578, i500, o3578) → f4306_1_length_ConstantStackPush(EOS, o3461, o3576, o3578, i500, o3578, o3578)
f4306_0_length_ConstantStackPush(EOS, o3578, o3576, o3578) → f4307_0_length_ConstantStackPush(EOS, o3578, o3576, o3578)
f7271_0_length_Return(EOS, o3461, o6070, o6072, i500, o6072, i676) → f6433_0_length_Return(EOS, o3461, o6070, o6072, i500, o6072, i676)
f6433_0_length_Return(EOS, o5421, o5422, o5423, i500, o5423, i644) → f6464_0_main_LE(EOS, o5421, o5422, o5423, i500, i644)
f6464_0_main_LE(EOS, o5421, o5422, o5423, i500, i644) → f6480_0_main_LE(EOS, o5421, o5422, o5423, i500, i644)
f6464_0_main_LE(EOS, o5421, o5422, o5423, i500, i644) → f6481_0_main_LE(EOS, o5421, o5422, o5423, i500, i644)
f6480_0_main_LE(EOS, o5421, o5422, o5423, i500, i644) → f6486_0_main_Load(EOS, o5421, o5422, o5423) | <=(i500, i644)
f6486_0_main_Load(EOS, o5421, o5422, o5423) → f6505_0_main_NONNULL(EOS, o5421, o5422, o5423, o5423)
f6505_0_main_NONNULL(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(o5460sub)) → f6516_0_main_NONNULL(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(o5460sub))
f6516_0_main_NONNULL(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(o5460sub)) → f6541_0_main_New(EOS, o5421, o5422, java.lang.Object(o5460sub))
f6541_0_main_New(EOS, o5421, o5422, java.lang.Object(o5460sub)) → f6572_0_main_Duplicate(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)))
f6572_0_main_Duplicate(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL))) → f6599_0_main_New(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
f6599_0_main_New(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → f6635_0_main_Duplicate(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f6635_0_main_Duplicate(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f6671_0_main_InvokeMethod(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), java.lang.Object(EOC))
f6671_0_main_InvokeMethod(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), java.lang.Object(EOC)) → f6728_0_main_Load(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f6728_0_main_Load(EOS, o5421, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f6800_0_main_InvokeMethod(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421)
f6800_0_main_InvokeMethod(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421) → f6891_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421)
f6891_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421) → f6935_0__init__InvokeMethod(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)))
f6935_0__init__InvokeMethod(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL))) → f6945_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421)
f6945_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421) → f6963_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)))
f6963_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL))) → f6975_0__init__FieldAccess(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f6975_0__init__FieldAccess(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f6993_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421)
f6993_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421) → f7039_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, o5421, java.lang.Object(List(EOC, NULL)))
f7039_0__init__Load(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, o5421, java.lang.Object(List(EOC, NULL))) → f7044_0__init__FieldAccess(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421)
f7044_0__init__FieldAccess(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5421, java.lang.Object(List(EOC, NULL)), o5421) → f7052_0__init__Return(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5421)), java.lang.Object(EOC), o5421)
f7052_0__init__Return(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5421)), java.lang.Object(EOC), o5421) → f7063_0_main_Store(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5421)))
f7063_0_main_Store(EOS, o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5421))) → f7072_0_main_New(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub))
f7072_0_main_New(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub)) → f7081_0_main_Duplicate(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)))
f7081_0_main_Duplicate(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL))) → f7088_0_main_New(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)))
f7088_0_main_New(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL))) → f7116_0_main_Duplicate(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f7116_0_main_Duplicate(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f7190_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), java.lang.Object(EOC))
f7190_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), java.lang.Object(EOC)) → f7284_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f7284_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), o5422, java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f7294_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422)
f7294_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422) → f7311_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422)
f7311_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422) → f7325_0__init__InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)))
f7325_0__init__InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL))) → f7330_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422)
f7330_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422) → f7335_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)))
f7335_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL))) → f7348_0__init__FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC))
f7348_0__init__FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422, java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC)) → f7357_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422)
f7357_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422) → f7365_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, o5422, java.lang.Object(List(EOC, NULL)))
f7365_0__init__Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, o5422, java.lang.Object(List(EOC, NULL))) → f7374_0__init__FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422)
f7374_0__init__FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, NULL)), java.lang.Object(List(EOC, NULL)), java.lang.Object(EOC), o5422, java.lang.Object(List(EOC, NULL)), o5422) → f7379_0__init__Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o5422)), java.lang.Object(EOC), o5422)
f7379_0__init__Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o5422)), java.lang.Object(EOC), o5422) → f7386_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5422)))
f7386_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(o5460sub), java.lang.Object(List(EOC, o5422))) → f7390_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub))
f7390_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub)) → f7395_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub))
f7395_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub)) → f7401_0_getTail_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub), java.lang.Object(o5460sub))
f7401_0_getTail_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub), java.lang.Object(o5460sub)) → f7416_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub), java.lang.Object(o5460sub))
f7416_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub), java.lang.Object(o5460sub)) → f7430_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(o5460sub), java.lang.Object(o5460sub))
f7416_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(o6242sub))), java.lang.Object(o6242sub), java.lang.Object(o6242sub)) → f7431_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(o6242sub))), java.lang.Object(o6242sub), java.lang.Object(o6242sub))
f7430_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o6249)), java.lang.Object(List(EOC, o6249))) → f7443_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o6249)), java.lang.Object(List(EOC, o6249)))
f7443_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o6249)), java.lang.Object(List(EOC, o6249))) → f7461_0_getTail_Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o6249)), o6249)
f7461_0_getTail_Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), java.lang.Object(List(EOC, o6249)), o6249) → f7480_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249)
f7480_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249) → f7509_0_main_JMP(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249)
f7509_0_main_JMP(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249) → f7544_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249)
f7544_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249) → f2582_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, o5422)), o6249)
f2582_0_main_Load(EOS, o1621, o1622, o1623) → f2589_0_main_InvokeMethod(EOS, o1621, o1622, o1623, o1621)
f7431_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), java.lang.Object(List(EOC, o6255)), java.lang.Object(List(EOC, o6255))) → f7447_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), java.lang.Object(List(EOC, o6255)), java.lang.Object(List(EOC, o6255)))
f7447_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), java.lang.Object(List(EOC, o6255)), java.lang.Object(List(EOC, o6255))) → f7476_0_getTail_Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), java.lang.Object(List(EOC, o6255)), o6255)
f7476_0_getTail_Return(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), java.lang.Object(List(EOC, o6255)), o6255) → f7487_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255)
f7487_0_main_Store(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255) → f7529_0_main_JMP(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255)
f7529_0_main_JMP(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255) → f7557_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255)
f7557_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255) → f2582_0_main_Load(EOS, java.lang.Object(List(EOC, o5421)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o6255)))), o6255)
f6481_0_main_LE(EOS, o5421, o5422, o5423, i500, i644) → f6500_0_main_Load(EOS, o5421, o5422, o5423) | >(i500, i644)
f6500_0_main_Load(EOS, o5421, o5422, o5423) → f6511_0_main_InvokeMethod(EOS, o5421, o5423, o5422)
f6511_0_main_InvokeMethod(EOS, o5421, o5423, java.lang.Object(o5464sub)) → f6535_0_main_InvokeMethod(EOS, o5421, o5423, java.lang.Object(o5464sub))
f6535_0_main_InvokeMethod(EOS, o5421, o5423, java.lang.Object(o5464sub)) → f6559_0_getTail_Load(EOS, o5421, o5423, java.lang.Object(o5464sub), java.lang.Object(o5464sub))
f6559_0_getTail_Load(EOS, o5421, o5423, java.lang.Object(o5464sub), java.lang.Object(o5464sub)) → f6624_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(o5464sub), java.lang.Object(o5464sub))
f6624_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(o5464sub), java.lang.Object(o5464sub)) → f6656_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(o5464sub), java.lang.Object(o5464sub))
f6624_0_getTail_FieldAccess(EOS, o5421, java.lang.Object(o5575sub), java.lang.Object(o5575sub), java.lang.Object(o5575sub)) → f6657_0_getTail_FieldAccess(EOS, o5421, java.lang.Object(o5575sub), java.lang.Object(o5575sub), java.lang.Object(o5575sub))
f6656_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(List(EOC, o5592)), java.lang.Object(List(EOC, o5592))) → f6677_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(List(EOC, o5592)), java.lang.Object(List(EOC, o5592)))
f6677_0_getTail_FieldAccess(EOS, o5421, o5423, java.lang.Object(List(EOC, o5592)), java.lang.Object(List(EOC, o5592))) → f6739_0_getTail_Return(EOS, o5421, o5423, java.lang.Object(List(EOC, o5592)), o5592)
f6739_0_getTail_Return(EOS, o5421, o5423, java.lang.Object(List(EOC, o5592)), o5592) → f6809_0_main_Store(EOS, o5421, o5423, o5592)
f6809_0_main_Store(EOS, o5421, o5423, o5592) → f6898_0_main_JMP(EOS, o5421, o5592, o5423)
f6898_0_main_JMP(EOS, o5421, o5592, o5423) → f6929_0_main_Load(EOS, o5421, o5592, o5423)
f6929_0_main_Load(EOS, o5421, o5592, o5423) → f2582_0_main_Load(EOS, o5421, o5592, o5423)
f6657_0_getTail_FieldAccess(EOS, o5421, java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643))) → f6699_0_getTail_FieldAccess(EOS, o5421, java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)))
f6699_0_getTail_FieldAccess(EOS, o5421, java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643))) → f6768_0_getTail_Return(EOS, o5421, java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)), o5643)
f6768_0_getTail_Return(EOS, o5421, java.lang.Object(List(EOC, o5643)), java.lang.Object(List(EOC, o5643)), o5643) → f6815_0_main_Store(EOS, o5421, java.lang.Object(List(EOC, o5643)), o5643)
f6815_0_main_Store(EOS, o5421, java.lang.Object(List(EOC, o5643)), o5643) → f6905_0_main_JMP(EOS, o5421, o5643, java.lang.Object(List(EOC, o5643)))
f6905_0_main_JMP(EOS, o5421, o5643, java.lang.Object(List(EOC, o5643))) → f6932_0_main_Load(EOS, o5421, o5643, java.lang.Object(List(EOC, o5643)))
f6932_0_main_Load(EOS, o5421, o5643, java.lang.Object(List(EOC, o5643))) → f2582_0_main_Load(EOS, o5421, o5643, java.lang.Object(List(EOC, o5643)))
f4181_0_main_NE(EOS, o3461, o3252, o3254, matching1, matching2) → f4186_0_main_Load(EOS, o3461, o3252, o3254) | &&(=(matching1, 1), =(matching2, 1))
f4186_0_main_Load(EOS, o3461, o3252, o3254) → f4199_0_main_InvokeMethod(EOS, o3252, o3254, o3461)
f4199_0_main_InvokeMethod(EOS, o3252, o3254, java.lang.Object(o3509sub)) → f4210_0_main_InvokeMethod(EOS, o3252, o3254, java.lang.Object(o3509sub))
f4210_0_main_InvokeMethod(EOS, o3252, o3254, java.lang.Object(o3509sub)) → f4224_0_getTail_Load(EOS, o3252, o3254, java.lang.Object(o3509sub), java.lang.Object(o3509sub))
f4224_0_getTail_Load(EOS, o3252, o3254, java.lang.Object(o3509sub), java.lang.Object(o3509sub)) → f4268_0_getTail_FieldAccess(EOS, o3252, o3254, java.lang.Object(o3509sub), java.lang.Object(o3509sub))
f4268_0_getTail_FieldAccess(EOS, o3252, o3254, java.lang.Object(List(EOC, o3564)), java.lang.Object(List(EOC, o3564))) → f4272_0_getTail_FieldAccess(EOS, o3252, o3254, java.lang.Object(List(EOC, o3564)), java.lang.Object(List(EOC, o3564)))
f4272_0_getTail_FieldAccess(EOS, o3252, o3254, java.lang.Object(List(EOC, o3564)), java.lang.Object(List(EOC, o3564))) → f4288_0_getTail_Return(EOS, o3252, o3254, java.lang.Object(List(EOC, o3564)), o3564)
f4288_0_getTail_Return(EOS, o3252, o3254, java.lang.Object(List(EOC, o3564)), o3564) → f4291_0_main_Store(EOS, o3252, o3254, o3564)
f4291_0_main_Store(EOS, o3252, o3254, o3564) → f4296_0_main_JMP(EOS, o3564, o3252, o3254)
f4296_0_main_JMP(EOS, o3564, o3252, o3254) → f4302_0_main_Load(EOS, o3564, o3252, o3254)
f4302_0_main_Load(EOS, o3564, o3252, o3254) → f2582_0_main_Load(EOS, o3564, o3252, o3254)
f2593_1_length_ConstantStackPush(EOS, o6019, o1622, o1623, o6019, o6019) → f7136_0_length_Return(EOS, o6019, o1622, o1623, o6019, i669)
f3632_1_length_ConstantStackPush(EOS, o2727, o6028, o6030, i418, o6028, o6028) → f7173_0_length_Return(EOS, o2727, o6028, o6030, i418, o6028, i670)
f4022_1_length_ConstantStackPush(EOS, o3180, o6038, o6040, i484, o6040, o6040) → f7198_0_length_Return(EOS, o3180, o6038, o6040, i484, o6040, i671)
f4116_1_length_ConstantStackPush(EOS, o6048, o3252, o3254, o6048, o6048) → f7221_0_length_Return(EOS, o6048, o3252, o3254, o6048, i673)
f4205_1_length_ConstantStackPush(EOS, o3461, o6057, o6059, o6057, o6057) → f7252_0_length_Return(EOS, o3461, o6057, o6059, o6057, i674)
f4306_1_length_ConstantStackPush(EOS, o3461, o6070, o6072, i500, o6072, o6072) → f7271_0_length_Return(EOS, o3461, o6070, o6072, i500, o6072, i676)

Combined rules. Obtained 11 IRules

P rules:
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f2596_0_length_ConstantStackPush(EOS, x0, x0)
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f3636_0_length_ConstantStackPush(EOS, x1, x2, x1)
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f4031_0_length_ConstantStackPush(EOS, x2, x1, x2)
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f4123_0_length_ConstantStackPush(EOS, x0, x0)
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f4216_0_length_ConstantStackPush(EOS, x1, x2, x1)
f2589_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), x1, x2, java.lang.Object(List(EOC, x0))) → f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0)
f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0) → f4307_0_length_ConstantStackPush(EOS, x2, x1, x2)
f2589_0_main_InvokeMethod(EOS, x0, x1, java.lang.Object(List(EOC, x2)), x0) → f2589_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x1)), x2, java.lang.Object(List(EOC, x0)))
f2589_0_main_InvokeMethod(EOS, x0, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x1)), x0) → f2589_0_main_InvokeMethod(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1)))), x1, java.lang.Object(List(EOC, x0)))
f2589_0_main_InvokeMethod(EOS, x0, java.lang.Object(List(EOC, x1)), x2, x0) → f2589_0_main_InvokeMethod(EOS, x0, x1, x2, x0)
f2589_0_main_InvokeMethod(EOS, x0, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x1)), x0) → f2589_0_main_InvokeMethod(EOS, x0, x1, java.lang.Object(List(EOC, x1)), x0)

Filtered ground terms:

f2589_0_main_InvokeMethod(x1, x2, x3, x4, x5) → f2589_0_main_InvokeMethod(x2, x3, x4, x5)
f2596_0_length_ConstantStackPush(x1, x2, x3) → f2596_0_length_ConstantStackPush(x2, x3)
f3636_0_length_ConstantStackPush(x1, x2, x3, x4) → f3636_0_length_ConstantStackPush(x2, x3, x4)
f4031_0_length_ConstantStackPush(x1, x2, x3, x4) → f4031_0_length_ConstantStackPush(x2, x3, x4)
f4123_0_length_ConstantStackPush(x1, x2, x3) → f4123_0_length_ConstantStackPush(x2, x3)
f4216_0_length_ConstantStackPush(x1, x2, x3, x4) → f4216_0_length_ConstantStackPush(x2, x3, x4)
f4307_0_length_ConstantStackPush(x1, x2, x3, x4) → f4307_0_length_ConstantStackPush(x2, x3, x4)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f2589_0_main_InvokeMethod(x1, x2, x3, x4) → f2589_0_main_InvokeMethod(x2, x3, x4)
f2596_0_length_ConstantStackPush(x1, x2) → f2596_0_length_ConstantStackPush(x2)
f3636_0_length_ConstantStackPush(x1, x2, x3) → f3636_0_length_ConstantStackPush(x2, x3)
f4031_0_length_ConstantStackPush(x1, x2, x3) → f4031_0_length_ConstantStackPush(x2, x3)
f4123_0_length_ConstantStackPush(x1, x2) → f4123_0_length_ConstantStackPush(x2)
f4216_0_length_ConstantStackPush(x1, x2, x3) → f4216_0_length_ConstantStackPush(x2, x3)
f4307_0_length_ConstantStackPush(x1, x2, x3) → f4307_0_length_ConstantStackPush(x2, x3)

Prepared 11 rules for path length conversion:

P rules:
f2589_0_main_InvokeMethod(x1, x2, x0) → f2596_0_length_ConstantStackPush(x0)
f2589_0_main_InvokeMethod(x1, x2, x0) → f3636_0_length_ConstantStackPush(x2, x1)
f2589_0_main_InvokeMethod(x1, x2, x0) → f4031_0_length_ConstantStackPush(x1, x2)
f2589_0_main_InvokeMethod(x1, x2, x0) → f4123_0_length_ConstantStackPush(x0)
f2589_0_main_InvokeMethod(x1, x2, x0) → f4216_0_length_ConstantStackPush(x2, x1)
f2589_0_main_InvokeMethod(x1, x2, java.lang.Object(List(x0))) → f2589_0_main_InvokeMethod(x1, x2, x0)
f2589_0_main_InvokeMethod(x1, x2, x0) → f4307_0_length_ConstantStackPush(x1, x2)
f2589_0_main_InvokeMethod(x1, java.lang.Object(List(x2)), x0) → f2589_0_main_InvokeMethod(java.lang.Object(List(x1)), x2, java.lang.Object(List(x0)))
f2589_0_main_InvokeMethod(java.lang.Object(List(x1)), java.lang.Object(List(x1)), x0) → f2589_0_main_InvokeMethod(java.lang.Object(List(java.lang.Object(List(x1)))), x1, java.lang.Object(List(x0)))
f2589_0_main_InvokeMethod(java.lang.Object(List(x1)), x2, x0) → f2589_0_main_InvokeMethod(x1, x2, x0)
f2589_0_main_InvokeMethod(java.lang.Object(List(x1)), java.lang.Object(List(x1)), x0) → f2589_0_main_InvokeMethod(x1, java.lang.Object(List(x1)), x0)

Finished conversion. Obtained 5 rules.

P rules:
f2589_0_main_InvokeMethod(v34, v35, v36) → f2589_0_main_InvokeMethod(v37, v38, v39) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v39, 1), 0), <=(+(v39, 1), v36)), >(+(v38, 1), 0)), <=(v38, v35)), >(+(v37, 1), 0)), <=(v37, v34)), >(+(v36, 1), 1)), >(+(v35, 1), 0)), >(+(v34, 1), 0))
f2589_0_main_InvokeMethod(v40, v41, v42) → f2589_0_main_InvokeMethod(v43, v44, v45) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v45, 1), 1), <=(-(v45, 2), v42)), >(+(v44, 1), 0)), <=(+(v44, 1), v41)), >(+(v43, 1), 1)), <=(-(v43, 2), v40)), >(+(v42, 1), 0)), >(+(v41, 1), 1)), >(+(v40, 1), 0))
f2589_0_main_InvokeMethod(v46, v47, v48) → f2589_0_main_InvokeMethod(v49, v50, v51) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v51, 1), 1), <=(-(v51, 2), v48)), >(+(v50, 1), 0)), <=(+(v50, 1), v47)), <=(+(v50, 1), v46)), >(+(v49, 1), 3)), <=(-(v49, 2), v47)), <=(-(v49, 2), v46)), >(+(v48, 1), 0)), >(+(v47, 1), 1)), >(+(v46, 1), 1))
f2589_0_main_InvokeMethod(v52, v53, v54) → f2589_0_main_InvokeMethod(v55, v56, v57) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v57, 1), 0), <=(v57, v54)), >(+(v56, 1), 0)), <=(v56, v53)), >(+(v55, 1), 0)), <=(+(v55, 1), v52)), >(+(v54, 1), 0)), >(+(v53, 1), 0)), >(+(v52, 1), 1))
f2589_0_main_InvokeMethod(v58, v59, v60) → f2589_0_main_InvokeMethod(v61, v62, v63) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v63, 1), 0), <=(v63, v60)), >(+(v62, 1), 1)), <=(v62, v59)), <=(v62, v58)), >(+(v61, 1), 0)), <=(+(v61, 1), v59)), <=(+(v61, 1), v58)), >(+(v60, 1), 0)), >(+(v59, 1), 1)), >(+(v58, 1), 1))

(17) Obligation:

Rules:
f2589_0_main_InvokeMethod(v34, v35, v36) → f2589_0_main_InvokeMethod(v37, v38, v39) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v39, 1), 0), <=(+(v39, 1), v36)), >(+(v38, 1), 0)), <=(v38, v35)), >(+(v37, 1), 0)), <=(v37, v34)), >(+(v36, 1), 1)), >(+(v35, 1), 0)), >(+(v34, 1), 0))
f2589_0_main_InvokeMethod(v40, v41, v42) → f2589_0_main_InvokeMethod(v43, v44, v45) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v45, 1), 1), <=(-(v45, 2), v42)), >(+(v44, 1), 0)), <=(+(v44, 1), v41)), >(+(v43, 1), 1)), <=(-(v43, 2), v40)), >(+(v42, 1), 0)), >(+(v41, 1), 1)), >(+(v40, 1), 0))
f2589_0_main_InvokeMethod(v46, v47, v48) → f2589_0_main_InvokeMethod(v49, v50, v51) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v51, 1), 1), <=(-(v51, 2), v48)), >(+(v50, 1), 0)), <=(+(v50, 1), v47)), <=(+(v50, 1), v46)), >(+(v49, 1), 3)), <=(-(v49, 2), v47)), <=(-(v49, 2), v46)), >(+(v48, 1), 0)), >(+(v47, 1), 1)), >(+(v46, 1), 1))
f2589_0_main_InvokeMethod(v52, v53, v54) → f2589_0_main_InvokeMethod(v55, v56, v57) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v57, 1), 0), <=(v57, v54)), >(+(v56, 1), 0)), <=(v56, v53)), >(+(v55, 1), 0)), <=(+(v55, 1), v52)), >(+(v54, 1), 0)), >(+(v53, 1), 0)), >(+(v52, 1), 1))
f2589_0_main_InvokeMethod(v58, v59, v60) → f2589_0_main_InvokeMethod(v61, v62, v63) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v63, 1), 0), <=(v63, v60)), >(+(v62, 1), 1)), <=(v62, v59)), <=(v62, v58)), >(+(v61, 1), 0)), <=(+(v61, 1), v59)), <=(+(v61, 1), v58)), >(+(v60, 1), 0)), >(+(v59, 1), 1)), >(+(v58, 1), 1))

(18) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f2589_0_main_InvokeMethod(x)] = 1·x₁ + 5·x₂ + 1·x₃

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f2589_0_main_InvokeMethod(x0, x1, x2) → f2589_0_main_InvokeMethod(x3, x4, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x5, 1), 0), <=(+(x5, 1), x2)), >(+(x4, 1), 0)), <=(x4, x1)), >(+(x3, 1), 0)), <=(x3, x0)), >(+(x2, 1), 1)), >(+(x1, 1), 0)), >(+(x0, 1), 0))
f2589_0_main_InvokeMethod(x6, x7, x8) → f2589_0_main_InvokeMethod(x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 1), <=(-(x11, 2), x8)), >(+(x10, 1), 0)), <=(+(x10, 1), x7)), >(+(x9, 1), 1)), <=(-(x9, 2), x6)), >(+(x8, 1), 0)), >(+(x7, 1), 1)), >(+(x6, 1), 0))
f2589_0_main_InvokeMethod(x12, x13, x14) → f2589_0_main_InvokeMethod(x15, x16, x17) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x17, 1), 1), <=(-(x17, 2), x14)), >(+(x16, 1), 0)), <=(+(x16, 1), x13)), <=(+(x16, 1), x12)), >(+(x15, 1), 3)), <=(-(x15, 2), x13)), <=(-(x15, 2), x12)), >(+(x14, 1), 0)), >(+(x13, 1), 1)), >(+(x12, 1), 1))
f2589_0_main_InvokeMethod(x18, x19, x20) → f2589_0_main_InvokeMethod(x21, x22, x23) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x23, 1), 0), <=(x23, x20)), >(+(x22, 1), 0)), <=(x22, x19)), >(+(x21, 1), 0)), <=(+(x21, 1), x18)), >(+(x20, 1), 0)), >(+(x19, 1), 0)), >(+(x18, 1), 1))
f2589_0_main_InvokeMethod(x24, x25, x26) → f2589_0_main_InvokeMethod(x27, x28, x29) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x29, 1), 0), <=(x29, x26)), >(+(x28, 1), 1)), <=(x28, x25)), <=(x28, x24)), >(+(x27, 1), 0)), <=(+(x27, 1), x25)), <=(+(x27, 1), x24)), >(+(x26, 1), 0)), >(+(x25, 1), 1)), >(+(x24, 1), 1))

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) LinearRankingProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) LinearRankingProcessor (EQUIVALENT transformation)

(19) YES