MAYBE Problem: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Proof: DP Processor: DPs: gcd#(x,y) -> gcd2#(x,y,0()) gcd2#(x,y,i) -> inc#(i) gcd2#(x,y,i) -> le#(y,x) gcd2#(x,y,i) -> le#(x,y) gcd2#(x,y,i) -> le#(y,0()) gcd2#(x,y,i) -> le#(x,0()) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) if3#(false(),b3,x,y,i) -> minus#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if4#(false(),x,y,i) -> minus#(y,x) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) inc#(s(i)) -> inc#(i) le#(s(x),s(y)) -> le#(x,y) minus#(s(x),s(y)) -> minus#(x,y) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() TDG Processor: DPs: gcd#(x,y) -> gcd2#(x,y,0()) gcd2#(x,y,i) -> inc#(i) gcd2#(x,y,i) -> le#(y,x) gcd2#(x,y,i) -> le#(x,y) gcd2#(x,y,i) -> le#(y,0()) gcd2#(x,y,i) -> le#(x,0()) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) if3#(false(),b3,x,y,i) -> minus#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if4#(false(),x,y,i) -> minus#(y,x) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) inc#(s(i)) -> inc#(i) le#(s(x),s(y)) -> le#(x,y) minus#(s(x),s(y)) -> minus#(x,y) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() graph: if4#(false(),x,y,i) -> minus#(y,x) -> minus#(s(x),s(y)) -> minus#(x,y) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(x,0()) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(y,0()) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(x,y) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(y,x) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> inc#(i) minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) if3#(false(),b3,x,y,i) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(x,0()) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(y,0()) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(y,x) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> inc#(i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) -> if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) -> if4#(false(),x,y,i) -> minus#(y,x) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(false(),b3,x,y,i) -> minus#(x,y) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) -> if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) inc#(s(i)) -> inc#(i) -> inc#(s(i)) -> inc#(i) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) -> if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) gcd2#(x,y,i) -> le#(y,0()) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> le#(y,x) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> le#(x,0()) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> inc#(i) -> inc#(s(i)) -> inc#(i) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(x,0()) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(y,0()) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(x,y) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(y,x) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> inc#(i) EDG Processor: DPs: gcd#(x,y) -> gcd2#(x,y,0()) gcd2#(x,y,i) -> inc#(i) gcd2#(x,y,i) -> le#(y,x) gcd2#(x,y,i) -> le#(x,y) gcd2#(x,y,i) -> le#(y,0()) gcd2#(x,y,i) -> le#(x,0()) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) if3#(false(),b3,x,y,i) -> minus#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if4#(false(),x,y,i) -> minus#(y,x) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) inc#(s(i)) -> inc#(i) le#(s(x),s(y)) -> le#(x,y) minus#(s(x),s(y)) -> minus#(x,y) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() graph: if4#(false(),x,y,i) -> minus#(y,x) -> minus#(s(x),s(y)) -> minus#(x,y) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> inc#(i) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(y,x) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(x,y) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(y,0()) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> le#(x,0()) if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) if3#(false(),b3,x,y,i) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> inc#(i) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(y,x) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(x,y) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(y,0()) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> le#(x,0()) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) -> if4#(false(),x,y,i) -> minus#(y,x) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) -> if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(false(),b3,x,y,i) -> minus#(x,y) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) -> if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) -> if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) inc#(s(i)) -> inc#(i) -> inc#(s(i)) -> inc#(i) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) -> if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) gcd2#(x,y,i) -> le#(y,x) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) gcd2#(x,y,i) -> inc#(i) -> inc#(s(i)) -> inc#(i) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> inc#(i) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(y,x) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(x,y) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(y,0()) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> le#(x,0()) gcd#(x,y) -> gcd2#(x,y,0()) -> gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) SCC Processor: #sccs: 4 #rules: 9 #arcs: 33/289 DPs: if4#(false(),x,y,i) -> gcd2#(x,minus(y,x),i) gcd2#(x,y,i) -> if1#(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1#(false(),b1,b2,b3,x,y,i) -> if2#(b1,b2,b3,x,y,i) if2#(false(),b2,b3,x,y,i) -> if3#(b2,b3,x,y,i) if3#(true(),b3,x,y,i) -> if4#(b3,x,y,i) if3#(false(),b3,x,y,i) -> gcd2#(minus(x,y),y,i) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Open DPs: inc#(s(i)) -> inc#(i) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Matrix Interpretation Processor: dim=1 interpretation: [inc#](x0) = 4x0 + 2, [c] = 4, [b] = 0, [a] = 4, [s](x0) = x0 + 4, [if4](x0, x1, x2, x3) = 0, [minus](x0, x1) = x0, [if3](x0, x1, x2, x3, x4) = 0, [if2](x0, x1, x2, x3, x4, x5) = 0, [false] = 0, [pair](x0, x1) = 0, [neededIterations](x0) = 0, [result](x0) = 0, [true] = 0, [if1](x0, x1, x2, x3, x4, x5, x6) = 0, [inc](x0) = 4x0 + 2, [le](x0, x1) = 0, [gcd2](x0, x1, x2) = 0, [0] = 0, [gcd](x0, x1) = 4 orientation: inc#(s(i)) = 4i + 18 >= 4i + 2 = inc#(i) gcd(x,y) = 4 >= 0 = gcd2(x,y,0()) gcd2(x,y,i) = 0 >= 0 = if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) = 0 >= 0 = pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) = 0 >= 0 = if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) = 0 >= 0 = if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) = 0 >= 0 = gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) = 0 >= 0 = if4(b3,x,y,i) if4(false(),x,y,i) = 0 >= 0 = gcd2(x,minus(y,x),i) if4(true(),x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) inc(0()) = 2 >= 0 = 0() inc(s(i)) = 4i + 18 >= 4i + 6 = s(inc(i)) le(s(x),0()) = 0 >= 0 = false() le(0(),y) = 0 >= 0 = true() le(s(x),s(y)) = 0 >= 0 = le(x,y) minus(x,0()) = x >= x = x minus(0(),y) = 0 >= 0 = 0() minus(s(x),s(y)) = x + 4 >= x = minus(x,y) a() = 4 >= 0 = b() a() = 4 >= 4 = c() problem: DPs: TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Matrix Interpretation Processor: dim=1 interpretation: [le#](x0, x1) = x1 + 1/2, [c] = 0, [b] = 0, [a] = 1/2, [s](x0) = 2x0 + 1, [if4](x0, x1, x2, x3) = 0, [minus](x0, x1) = x0, [if3](x0, x1, x2, x3, x4) = 0, [if2](x0, x1, x2, x3, x4, x5) = 0, [false] = 2, [pair](x0, x1) = 0, [neededIterations](x0) = 0, [result](x0) = 0, [true] = 0, [if1](x0, x1, x2, x3, x4, x5, x6) = 0, [inc](x0) = 2x0, [le](x0, x1) = x0 + x1 + 1/2, [gcd2](x0, x1, x2) = 0, [0] = 1/2, [gcd](x0, x1) = 2x0 + 1/2 orientation: le#(s(x),s(y)) = 2y + 3/2 >= y + 1/2 = le#(x,y) gcd(x,y) = 2x + 1/2 >= 0 = gcd2(x,y,0()) gcd2(x,y,i) = 0 >= 0 = if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) = 0 >= 0 = pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) = 0 >= 0 = if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) = 0 >= 0 = if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) = 0 >= 0 = gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) = 0 >= 0 = if4(b3,x,y,i) if4(false(),x,y,i) = 0 >= 0 = gcd2(x,minus(y,x),i) if4(true(),x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) inc(0()) = 1 >= 1/2 = 0() inc(s(i)) = 4i + 2 >= 4i + 1 = s(inc(i)) le(s(x),0()) = 2x + 2 >= 2 = false() le(0(),y) = y + 1 >= 0 = true() le(s(x),s(y)) = 2x + 2y + 5/2 >= x + y + 1/2 = le(x,y) minus(x,0()) = x >= x = x minus(0(),y) = 1/2 >= 1/2 = 0() minus(s(x),s(y)) = 2x + 1 >= x = minus(x,y) a() = 1/2 >= 0 = b() a() = 1/2 >= 0 = c() problem: DPs: TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Qed DPs: minus#(s(x),s(y)) -> minus#(x,y) TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Matrix Interpretation Processor: dim=1 interpretation: [minus#](x0, x1) = x0, [c] = 2, [b] = 0, [a] = 2, [s](x0) = 4x0 + 1, [if4](x0, x1, x2, x3) = 0, [minus](x0, x1) = 2x0 + x1, [if3](x0, x1, x2, x3, x4) = 0, [if2](x0, x1, x2, x3, x4, x5) = 0, [false] = 2, [pair](x0, x1) = 0, [neededIterations](x0) = 0, [result](x0) = 0, [true] = 0, [if1](x0, x1, x2, x3, x4, x5, x6) = 0, [inc](x0) = 4x0 + 1, [le](x0, x1) = x0 + 1, [gcd2](x0, x1, x2) = 0, [0] = 0, [gcd](x0, x1) = 2x0 + 2x1 orientation: minus#(s(x),s(y)) = 4x + 1 >= x = minus#(x,y) gcd(x,y) = 2x + 2y >= 0 = gcd2(x,y,0()) gcd2(x,y,i) = 0 >= 0 = if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) = 0 >= 0 = pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) = 0 >= 0 = if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) = 0 >= 0 = if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) = 0 >= 0 = gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) = 0 >= 0 = if4(b3,x,y,i) if4(false(),x,y,i) = 0 >= 0 = gcd2(x,minus(y,x),i) if4(true(),x,y,i) = 0 >= 0 = pair(result(x),neededIterations(i)) inc(0()) = 1 >= 0 = 0() inc(s(i)) = 16i + 5 >= 16i + 5 = s(inc(i)) le(s(x),0()) = 4x + 2 >= 2 = false() le(0(),y) = 1 >= 0 = true() le(s(x),s(y)) = 4x + 2 >= x + 1 = le(x,y) minus(x,0()) = 2x >= x = x minus(0(),y) = y >= 0 = 0() minus(s(x),s(y)) = 8x + 4y + 3 >= 2x + y = minus(x,y) a() = 2 >= 0 = b() a() = 2 >= 2 = c() problem: DPs: TRS: gcd(x,y) -> gcd2(x,y,0()) gcd2(x,y,i) -> if1(le(x,0()),le(y,0()),le(x,y),le(y,x),x,y,inc(i)) if1(true(),b1,b2,b3,x,y,i) -> pair(result(y),neededIterations(i)) if1(false(),b1,b2,b3,x,y,i) -> if2(b1,b2,b3,x,y,i) if2(true(),b2,b3,x,y,i) -> pair(result(x),neededIterations(i)) if2(false(),b2,b3,x,y,i) -> if3(b2,b3,x,y,i) if3(false(),b3,x,y,i) -> gcd2(minus(x,y),y,i) if3(true(),b3,x,y,i) -> if4(b3,x,y,i) if4(false(),x,y,i) -> gcd2(x,minus(y,x),i) if4(true(),x,y,i) -> pair(result(x),neededIterations(i)) inc(0()) -> 0() inc(s(i)) -> s(inc(i)) le(s(x),0()) -> false() le(0(),y) -> true() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(0(),y) -> 0() minus(s(x),s(y)) -> minus(x,y) a() -> b() a() -> c() Qed