Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 368 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 1 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 64 ms)
        ↳7 intTRS
        ↳8 TerminationGraphProcessor (⇒, 0 ms)
        ↳9 AND
            ↳10 intTRS
                ↳11 PolynomialOrderProcessor (⇔, 0 ms)
                ↳12 YES
            ↳13 intTRS
                ↳14 PolynomialOrderProcessor (⇔, 0 ms)
                ↳15 YES
    ↳16 JBCTerminationSCC
        ↳17 SCCToIntTRSProof (⇒, 0 ms)
        ↳18 intTRS
        ↳19 PolynomialOrderProcessor (⇔, 0 ms)
        ↳20 YES

(0) Obligation:

JBC Problem based on JBC Program:
/**
 * This class represents a list. The function get(n) can be used to access
 * the n-th element. 
 * @author Marc Brockschmidt
 */
public class CyclicList {
	/**
	 * A reference to the next list element.
	 */
	private CyclicList next;
	
	public static void main(String[] args) {
		CyclicList list = CyclicList.create(args.length);
		list.get(args[0].length());
	}
	
	/**
	 * Create a new list element.
	 * @param n a reference to the next element.
	 */
	public CyclicList(final CyclicList n) {
		this.next = n;
	}
	
	/**
	 * Create a new cyclical list of a length l.
	 * @param l some length
	 * @return cyclical list of length max(1, l)
	 */
	public static CyclicList create(int x) {
		CyclicList last, current;
		last = current = new CyclicList(null);
		while (--x > 0)
			current = new CyclicList(current);
		return last.next = current;
	}

	public CyclicList get(int n) {
		CyclicList cur = this;
		while (--n > 0) {
			cur = cur.next;
		}
		return cur;
	}	
}



(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CyclicList.main([Ljava/lang/String;)V: Graph of 155 nodes with 2 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: CyclicList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • CyclicList: [next]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f829_0_get_Load(EOS, i142, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f838_0_get_LE(EOS, i142, i142, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149)
f838_0_get_LE(EOS, i153, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f846_0_get_LE(EOS, i153, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149)
f846_0_get_LE(EOS, i153, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f856_0_get_Load(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) | >(i153, 0)
f856_0_get_Load(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f865_0_get_FieldAccess(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149)
f865_0_get_FieldAccess(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f885_0_get_FieldAccess(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) | &&(&&(&&(>(o149[CyclicList.next]o150, 0), >(o150[CyclicList.next]o149, 0)), >(o150[CyclicList.next]o150, 0)), >(o149[CyclicList.next]o149, 0))
f865_0_get_FieldAccess(EOS, i153, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o165[CyclicList.next]o165, o165[CyclicList.next]o165) → f886_0_get_FieldAccess(EOS, i153, o165[CyclicList.next]o165)
f885_0_get_FieldAccess(EOS, i153, o167[CyclicList.next]o150, o150[CyclicList.next]o167, o150[CyclicList.next]o150, o167[CyclicList.next]o167) → f895_0_get_FieldAccess(EOS, i153, o150[CyclicList.next]o150, o150[CyclicList.next]o167, o168[CyclicList.next]o150, o168[CyclicList.next]o167) | &&(=(o168[CyclicList.next]o150, +(o167[CyclicList.next]o150, -1)), =(o168[CyclicList.next]o167, +(o167[CyclicList.next]o167, -1)))
f895_0_get_FieldAccess(EOS, i153, o150[CyclicList.next]o150, o150[CyclicList.next]o167, o168[CyclicList.next]o150, o168[CyclicList.next]o167) → f901_0_get_Store(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168)
f901_0_get_Store(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168) → f907_0_get_JMP(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168)
f907_0_get_JMP(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168) → f923_0_get_Inc(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168)
f923_0_get_Inc(EOS, i153, o150[CyclicList.next]o150, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o168[CyclicList.next]o168) → f820_0_get_Inc(EOS, i153, o168[CyclicList.next]o150, o150[CyclicList.next]o168, o150[CyclicList.next]o150, o168[CyclicList.next]o168)
f820_0_get_Inc(EOS, i136, o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) → f829_0_get_Load(EOS, +(i136, -1), o149[CyclicList.next]o150, o150[CyclicList.next]o149, o150[CyclicList.next]o150, o149[CyclicList.next]o149) | >=(i136, 0)
f886_0_get_FieldAccess(EOS, i153, o169[CyclicList.next]o169) → f897_0_get_FieldAccess(EOS, i153, o170[CyclicList.next]o169) | =(o170[CyclicList.next]o169, +(o169[CyclicList.next]o169, -1))
f897_0_get_FieldAccess(EOS, i153, o170[CyclicList.next]o169) → f905_0_get_Store(EOS, i153, o170[CyclicList.next]o169)
f905_0_get_Store(EOS, i153, o170[CyclicList.next]o169) → f910_0_get_JMP(EOS, i153, o170[CyclicList.next]o169)
f910_0_get_JMP(EOS, i153, o170[CyclicList.next]o169) → f933_0_get_Inc(EOS, i153, o170[CyclicList.next]o169)
f933_0_get_Inc(EOS, i153, o170[CyclicList.next]o169) → f820_0_get_Inc(EOS, i153, o170[CyclicList.next]o169, o169[CyclicList.next]o170, o169[CyclicList.next]o169, o170[CyclicList.next]o170) | &&(&&(=(o169[CyclicList.next]o170, 1), =(o169[CyclicList.next]o169, 0)), =(o170[CyclicList.next]o170, 0))

Combined rules. Obtained 2 IRules

P rules:
f829_0_get_Load(EOS, x0, x1, x2, x3, x4) → f829_0_get_Load(EOS, -(x0, 1), -(x1, 1), x6, x3, x7) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))
f829_0_get_Load(EOS, x0, x1, x2, x3, x3) → f829_0_get_Load(EOS, -(x0, 1), -(x3, 1), 1, 0, 0) | >(x0, 0)

Filtered ground terms:


f829_0_get_Load(x1, x2, x3, x4, x5, x6) → f829_0_get_Load(x2, x3, x4, x5, x6)
Cond_f829_0_get_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f829_0_get_Load(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f829_0_get_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f829_0_get_Load1(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


Cond_f829_0_get_Load1(x1, x2, x3, x4, x5, x6) → Cond_f829_0_get_Load1(x1, x2, x3, x4, x6)

Filtered unneeded terms:


Cond_f829_0_get_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f829_0_get_Load(x1, x2, x3, x5, x7, x8)
Cond_f829_0_get_Load1(x1, x2, x3, x4, x5) → Cond_f829_0_get_Load1(x1, x2, x5)

Prepared 2 rules for path length conversion:

P rules:
f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x1, 1), x6, x3, x7) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))
f829_0_get_Load(x0, x1, x2, x3, x3) → f829_0_get_Load(-(x0, 1), -(x3, 1), 1, 0, 0) | >(x0, 0)

Finished conversion. Obtained 2 rules.

P rules:
f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x1, 1), x5, x3, x6) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))
f829_0_get_Load(x7, x8, x9, x10, x101) → f829_0_get_Load(-(x7, 1), -(x10, 1), 1, 0, 0) | &&(>(x7, 0), =(x10, x101))

(7) Obligation:

Rules:
f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x1, 1), x5, x3, x6) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))
f829_0_get_Load(x7, x8, x9, x10, x101) → f829_0_get_Load(-(x7, 1), -(x10, 1), 1, 0, 0) | &&(>(x7, 0), =(x10, x101))

(8) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained 2 non-trivial SCCs.


(9) Complex Obligation (AND)

(10) Obligation:

Rules:
f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x1, 1), x5, x3, x6) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))

(11) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f829_0_get_Load(x8, x10, x12, x14, x16)] = x8

Therefore the following rule(s) have been dropped:


f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x1, 1), x5, x3, x6) | &&(&&(&&(&&(>(x4, 0), >(x3, 0)), >(x2, 0)), >(x0, 0)), >(x1, 0))

(12) YES

(13) Obligation:

Rules:
f829_0_get_Load(x7, x8, x9, x10, x11) → f829_0_get_Load(-(x7, 1), -(x10, 1), 1, 0, 0) | &&(>(x7, 0), =(x10, x11))

(14) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f829_0_get_Load(x6, x8, x10, x12, x14)] = x6

Therefore the following rule(s) have been dropped:


f829_0_get_Load(x0, x1, x2, x3, x4) → f829_0_get_Load(-(x0, 1), -(x3, 1), 1, 0, 0) | &&(>(x0, 0), =(x3, x4))

(15) YES

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CyclicList.main([Ljava/lang/String;)V
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:

(17) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 17 IRules

P rules:
f213_0_create_Load(EOS, i26, o32[CyclicList.next]o31) → f215_0_create_LE(EOS, i26, i26, o32[CyclicList.next]o31)
f215_0_create_LE(EOS, i31, i31, o32[CyclicList.next]o31) → f218_0_create_LE(EOS, i31, i31, o32[CyclicList.next]o31)
f218_0_create_LE(EOS, i31, i31, o32[CyclicList.next]o31) → f223_0_create_New(EOS, i31, o32[CyclicList.next]o31) | >(i31, 0)
f223_0_create_New(EOS, i31, o32[CyclicList.next]o31) → f228_0_create_Duplicate(EOS, i31, o32[CyclicList.next]o31)
f228_0_create_Duplicate(EOS, i31, o32[CyclicList.next]o31) → f231_0_create_Load(EOS, i31, o32[CyclicList.next]o31)
f231_0_create_Load(EOS, i31, o32[CyclicList.next]o31) → f233_0_create_InvokeMethod(EOS, i31, o32[CyclicList.next]o31)
f233_0_create_InvokeMethod(EOS, i31, o32[CyclicList.next]o31) → f259_0__init__Load(EOS, i31, o32[CyclicList.next]o31)
f259_0__init__Load(EOS, i31, o32[CyclicList.next]o31) → f280_0__init__InvokeMethod(EOS, i31, o32[CyclicList.next]o31)
f280_0__init__InvokeMethod(EOS, i31, o32[CyclicList.next]o31) → f290_0__init__Load(EOS, i31, o32[CyclicList.next]o31)
f290_0__init__Load(EOS, i31, o32[CyclicList.next]o31) → f298_0__init__Load(EOS, i31, o32[CyclicList.next]o31)
f298_0__init__Load(EOS, i31, o32[CyclicList.next]o31) → f306_0__init__FieldAccess(EOS, i31, o32[CyclicList.next]o31)
f306_0__init__FieldAccess(EOS, i31, o32[CyclicList.next]o31) → f325_0__init__Return(EOS, i31, o32[CyclicList.next]o31)
f325_0__init__Return(EOS, i31, o32[CyclicList.next]o31) → f330_0_create_Store(EOS, i31, o32[CyclicList.next]o31)
f330_0_create_Store(EOS, i31, o32[CyclicList.next]o31) → f338_0_create_JMP(EOS, i31, o32[CyclicList.next]o31)
f338_0_create_JMP(EOS, i31, o32[CyclicList.next]o31) → f367_0_create_Inc(EOS, i31, o32[CyclicList.next]o31)
f367_0_create_Inc(EOS, i31, o32[CyclicList.next]o31) → f207_0_create_Inc(EOS, i31, o40[CyclicList.next]o31)
f207_0_create_Inc(EOS, i20, o32[CyclicList.next]o31) → f213_0_create_Load(EOS, +(i20, -1), o32[CyclicList.next]o31) | >=(i20, 0)

Combined rules. Obtained 1 IRules

P rules:
f213_0_create_Load(EOS, x0, x1) → f213_0_create_Load(EOS, -(x0, 1), x2) | >(x0, 0)

Filtered ground terms:


f213_0_create_Load(x1, x2, x3) → f213_0_create_Load(x2, x3)
Cond_f213_0_create_Load(x1, x2, x3, x4, x5) → Cond_f213_0_create_Load(x1, x3, x4, x5)

Filtered unneeded terms:


Cond_f213_0_create_Load(x1, x2, x3, x4) → Cond_f213_0_create_Load(x1, x2)
f213_0_create_Load(x1, x2) → f213_0_create_Load(x1)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(18) Obligation:

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

(19) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f213_0_create_Load(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(20) YES