0 JBC
↳1 JBCToGraph (⇒, 328 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 34 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇔, 1 ms)
↳8 YES
/**
* Java can do infinite data objects, too.
* Here we take the first n elements from an
* ascending infinite list of integer numbers.
*
* @author Carsten Fuhs
*/
public class Take {
public static int[] take(int n, MyIterator f) {
int[] result = new int[n];
for (int i = 0; i < n; ++i) {
if (f.hasNext()) {
result[i] = f.next();
}
else {
break;
}
}
return result;
}
public static void main(String args[]) {
int start = args[0].length();
int howMany = args[1].length();
From f = new From(start);
int[] firstHowMany = take(howMany, f);
}
}
interface MyIterator {
boolean hasNext();
int next();
}
class From implements MyIterator {
private int current;
public From(int start) {
this.current = start;
}
public boolean hasNext() {
return true;
}
public int next() {
return current++;
}
}
Generated rules. Obtained 26 IRules
P rules:
f812_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90) → f815_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53)
f815_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53) → f818_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53)
f818_0_take_GE(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90, i53) → f823_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | <(i90, i53)
f823_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f827_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90)
f827_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f832_0_hasNext_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90)
f832_0_hasNext_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f838_0_hasNext_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, 1)
f838_0_hasNext_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, matching1) → f840_0_take_EQ(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, 1) | =(matching1, 1)
f840_0_take_EQ(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, matching1) → f842_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | &&(>(1, 0), =(matching1, 1))
f842_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f844_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)))
f844_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53))) → f846_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f846_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f849_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f849_0_take_InvokeMethod(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f851_0_next_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f851_0_next_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f853_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f853_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f855_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f855_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f856_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f856_0_next_Duplicate(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f859_0_next_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f859_0_next_ConstantStackPush(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f861_0_next_IntArithmetic(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f861_0_next_IntArithmetic(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f863_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f863_0_next_FieldAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f866_0_next_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f866_0_next_Return(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f868_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f868_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f872_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90)
f872_0_take_ArrayAccess(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, java.lang.Object(ARRAY(i53)), i90) → f875_0_take_Inc(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) | <(i90, i53)
f875_0_take_Inc(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f880_0_take_JMP(EOS, i53, i53, java.lang.Object(ARRAY(i53)), +(i90, 1)) | >=(i90, 0)
f880_0_take_JMP(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99) → f904_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99)
f904_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99) → f808_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i99)
f808_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90) → f812_0_take_Load(EOS, i53, i53, java.lang.Object(ARRAY(i53)), i90, i90)
Combined rules. Obtained 1 IRules
P rules:
f812_0_take_Load(EOS, x0, x0, java.lang.Object(ARRAY(x0)), x1, x1) → f812_0_take_Load(EOS, x0, x0, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 0), <(x1, x0))
Filtered ground terms:
f812_0_take_Load(x1, x2, x3, x4, x5, x6) → f812_0_take_Load(x2, x3, x4, x5, x6)
Cond_f812_0_take_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f812_0_take_Load(x1, x3, x4, x5, x6, x7)
Filtered duplicate terms:
f812_0_take_Load(x1, x2, x3, x4, x5) → f812_0_take_Load(x3, x5)
Cond_f812_0_take_Load(x1, x2, x3, x4, x5, x6) → Cond_f812_0_take_Load(x1, x4, x6)
Prepared 1 rules for path length conversion:
P rules:
f812_0_take_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f812_0_take_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(>(+(x1, 1), 0), <(x1, x0))
Finished conversion. Obtained 1 rules.
P rules:
f812_0_take_Load(v5, x1, x0) → f812_0_take_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped: