9.88/3.39 MAYBE 9.88/3.39 9.88/3.39 Proof: 9.88/3.39 ConCon could not decide confluence of the system. 9.88/3.39 \cite{ALS94}, Theorem 4.1 does not apply. 9.88/3.39 This system is of type 3 or smaller. 9.88/3.39 This system is strongly deterministic. 9.88/3.39 This system is of type 3 or smaller. 9.88/3.39 This system is deterministic. 9.88/3.39 This system is non-terminating. 9.88/3.39 Call external tool: 9.88/3.39 ./ttt2.sh 9.88/3.39 Input: 9.88/3.39 (VAR x y z) 9.88/3.39 (RULES 9.88/3.39 iadd(add(x, y)) -> tp2(x, y) 9.88/3.39 gcd(y, z) -> ?2(iadd(z), y, z) 9.88/3.39 ?2(tp2(x, y), y, z) -> gcd(x, y) 9.88/3.39 gcd(0, x) -> x 9.88/3.39 gcd(z, y) -> ?1(iadd(z), z, y) 9.88/3.39 ?1(tp2(x, y), z, y) -> gcd(x, y) 9.88/3.39 iadd(y) -> tp2(0, y) 9.88/3.39 iadd(s(z)) -> ?3(iadd(z), z) 9.88/3.39 ?3(tp2(x, y), z) -> tp2(s(x), y) 9.88/3.39 gcd(x, 0) -> x 9.88/3.39 ) 9.88/3.39 9.88/3.39 Matrix Interpretation Processor: dim=2 9.88/3.39 9.88/3.39 interpretation: 9.88/3.39 [2 2] [2 0] 9.88/3.39 [?3](x0, x1) = [0 3]x0 + [2 0]x1, 9.88/3.39 9.88/3.39 [1 0] 9.88/3.39 [s](x0) = [2 3]x0, 9.88/3.40 9.88/3.40 [1 1] [1 0] [1 2] [0] 9.88/3.40 [?1](x0, x1, x2) = [0 1]x0 + [1 0]x1 + [0 0]x2 + [2], 9.88/3.40 9.88/3.40 [0] 9.88/3.40 [0] = [0], 9.88/3.40 9.88/3.40 [1 1] [1 3] [1 0] [0] 9.88/3.40 [?2](x0, x1, x2) = [0 1]x0 + [2 0]x1 + [0 0]x2 + [2], 9.88/3.40 9.88/3.40 [3 3] [3 3] [0] 9.88/3.40 [gcd](x0, x1) = [2 1]x0 + [0 1]x1 + [2], 9.88/3.40 9.88/3.40 [1 2] [2 0] 9.88/3.40 [tp2](x0, x1) = [2 1]x0 + [0 1]x1, 9.88/3.40 9.88/3.40 [2 2] 9.88/3.40 [iadd](x0) = [0 1]x0, 9.88/3.40 9.88/3.40 [1 1] [1 1] [1] 9.88/3.40 [add](x0, x1) = [2 1]x0 + [0 2]x1 + [0] 9.88/3.40 orientation: 9.88/3.40 [6 4] [2 6] [2] [1 2] [2 0] 9.88/3.40 iadd(add(x,y)) = [2 1]x + [0 2]y + [0] >= [2 1]x + [0 1]y = tp2(x,y) 9.88/3.40 9.88/3.40 [3 3] [3 3] [0] [1 3] [3 3] [0] 9.88/3.40 gcd(y,z) = [2 1]y + [0 1]z + [2] >= [2 0]y + [0 1]z + [2] = ?2(iadd(z),y,z) 9.88/3.40 9.88/3.40 [3 3] [3 4] [1 0] [0] [3 3] [3 3] [0] 9.88/3.40 ?2(tp2(x,y),y,z) = [2 1]x + [2 1]y + [0 0]z + [2] >= [2 1]x + [0 1]y + [2] = gcd(x,y) 9.88/3.40 9.88/3.40 [3 3] [0] 9.88/3.40 gcd(0(),x) = [0 1]x + [2] >= x = x 9.88/3.40 9.88/3.40 [3 3] [3 3] [0] [1 2] [3 3] [0] 9.88/3.40 gcd(z,y) = [0 1]y + [2 1]z + [2] >= [0 0]y + [1 1]z + [2] = ?1(iadd(z),z,y) 9.88/3.40 9.88/3.40 [3 3] [3 3] [1 0] [0] [3 3] [3 3] [0] 9.88/3.40 ?1(tp2(x,y),z,y) = [2 1]x + [0 1]y + [1 0]z + [2] >= [2 1]x + [0 1]y + [2] = gcd(x,y) 9.88/3.40 9.88/3.40 [2 2] [2 0] 9.88/3.40 iadd(y) = [0 1]y >= [0 1]y = tp2(0(),y) 9.88/3.40 9.88/3.40 [6 6] [6 6] 9.88/3.40 iadd(s(z)) = [2 3]z >= [2 3]z = ?3(iadd(z),z) 9.88/3.40 9.88/3.40 [6 6] [4 2] [2 0] [5 6] [2 0] 9.88/3.40 ?3(tp2(x,y),z) = [6 3]x + [0 3]y + [2 0]z >= [4 3]x + [0 1]y = tp2(s(x),y) 9.88/3.40 9.88/3.40 [3 3] [0] 9.88/3.40 gcd(x,0()) = [2 1]x + [2] >= x = x 9.88/3.40 problem: 9.88/3.40 gcd(y,z) -> ?2(iadd(z),y,z) 9.88/3.40 ?2(tp2(x,y),y,z) -> gcd(x,y) 9.88/3.40 gcd(0(),x) -> x 9.88/3.40 gcd(z,y) -> ?1(iadd(z),z,y) 9.88/3.40 ?1(tp2(x,y),z,y) -> gcd(x,y) 9.88/3.40 iadd(y) -> tp2(0(),y) 9.88/3.40 iadd(s(z)) -> ?3(iadd(z),z) 9.88/3.40 ?3(tp2(x,y),z) -> tp2(s(x),y) 9.88/3.40 gcd(x,0()) -> x 9.88/3.40 Matrix Interpretation Processor: dim=2 9.88/3.40 9.88/3.40 interpretation: 9.88/3.40 [2 0] [1 0] 9.88/3.40 [?3](x0, x1) = [0 3]x0 + [0 0]x1, 9.88/3.40 9.88/3.40 [2 0] 9.88/3.40 [s](x0) = [1 2]x0, 9.88/3.40 9.88/3.40 [2 2] [1 0] [1] 9.88/3.40 [?1](x0, x1, x2) = [0 2]x0 + [0 0]x1 + x2 + [0], 9.88/3.40 9.88/3.40 [0] 9.88/3.40 [0] = [0], 9.88/3.40 9.88/3.40 [2 2] [1 2] [1 0] [1] 9.88/3.40 [?2](x0, x1, x2) = [0 2]x0 + [0 1]x1 + [0 0]x2 + [0], 9.88/3.40 9.88/3.40 [3 2] [3 2] [1] 9.88/3.40 [gcd](x0, x1) = [0 1]x0 + [0 1]x1 + [0], 9.88/3.40 9.88/3.40 [1 0] [1 1] 9.88/3.40 [tp2](x0, x1) = [2 2]x0 + [0 0]x1, 9.88/3.40 9.88/3.40 [1 1] 9.88/3.40 [iadd](x0) = [0 0]x0 9.88/3.40 orientation: 9.88/3.40 [3 2] [3 2] [1] [1 2] [3 2] [1] 9.88/3.40 gcd(y,z) = [0 1]y + [0 1]z + [0] >= [0 1]y + [0 0]z + [0] = ?2(iadd(z),y,z) 9.88/3.40 9.88/3.40 [6 4] [3 4] [1 0] [1] [3 2] [3 2] [1] 9.88/3.40 ?2(tp2(x,y),y,z) = [4 4]x + [0 1]y + [0 0]z + [0] >= [0 1]x + [0 1]y + [0] = gcd(x,y) 9.88/3.40 9.88/3.40 [3 2] [1] 9.88/3.40 gcd(0(),x) = [0 1]x + [0] >= x = x 9.88/3.40 9.88/3.40 [3 2] [3 2] [1] [3 2] [1] 9.88/3.40 gcd(z,y) = [0 1]y + [0 1]z + [0] >= y + [0 0]z + [0] = ?1(iadd(z),z,y) 9.93/3.40 9.93/3.40 [6 4] [3 2] [1 0] [1] [3 2] [3 2] [1] 9.93/3.40 ?1(tp2(x,y),z,y) = [4 4]x + [0 1]y + [0 0]z + [0] >= [0 1]x + [0 1]y + [0] = gcd(x,y) 9.93/3.40 9.93/3.40 [1 1] [1 1] 9.93/3.40 iadd(y) = [0 0]y >= [0 0]y = tp2(0(),y) 9.93/3.40 9.93/3.40 [3 2] [3 2] 9.93/3.40 iadd(s(z)) = [0 0]z >= [0 0]z = ?3(iadd(z),z) 9.93/3.40 9.93/3.40 [2 0] [2 2] [1 0] [2 0] [1 1] 9.93/3.40 ?3(tp2(x,y),z) = [6 6]x + [0 0]y + [0 0]z >= [6 4]x + [0 0]y = tp2(s(x),y) 9.93/3.40 9.93/3.40 [3 2] [1] 9.93/3.40 gcd(x,0()) = [0 1]x + [0] >= x = x 9.93/3.40 problem: 9.93/3.40 gcd(y,z) -> ?2(iadd(z),y,z) 9.93/3.40 ?2(tp2(x,y),y,z) -> gcd(x,y) 9.93/3.40 gcd(z,y) -> ?1(iadd(z),z,y) 9.93/3.40 ?1(tp2(x,y),z,y) -> gcd(x,y) 9.93/3.40 iadd(y) -> tp2(0(),y) 9.93/3.40 iadd(s(z)) -> ?3(iadd(z),z) 9.93/3.40 ?3(tp2(x,y),z) -> tp2(s(x),y) 9.93/3.40 Unfolding Processor: 9.93/3.41 loop length: 3 9.93/3.41 terms: 9.93/3.41 gcd(0(),0()) 9.93/3.41 ?2(iadd(0()),0(),0()) 9.93/3.41 ?2(tp2(0(),0()),0(),0()) 9.93/3.41 context: [] 9.93/3.41 substitution: 9.93/3.41 9.93/3.41 Qed 9.93/3.41 ConCon could not decide if this system is quasi-decreasing. 9.93/3.41 \cite{O02}, p. 214, Proposition 7.2.50 does not apply. 9.93/3.41 This system is of type 3 or smaller. 9.93/3.41 This system is deterministic. 9.93/3.41 This system is non-terminating. 9.93/3.41 Call external tool: 9.93/3.41 ./ttt2.sh 9.93/3.41 Input: 9.93/3.41 (VAR x y z) 9.93/3.41 (RULES 9.93/3.41 iadd(add(x, y)) -> tp2(x, y) 9.93/3.41 gcd(y, z) -> ?2(iadd(z), y, z) 9.93/3.41 ?2(tp2(x, y), y, z) -> gcd(x, y) 9.93/3.41 gcd(0, x) -> x 9.93/3.41 gcd(z, y) -> ?1(iadd(z), z, y) 9.93/3.41 ?1(tp2(x, y), z, y) -> gcd(x, y) 9.93/3.41 iadd(y) -> tp2(0, y) 9.93/3.41 iadd(s(z)) -> ?3(iadd(z), z) 9.93/3.41 ?3(tp2(x, y), z) -> tp2(s(x), y) 9.93/3.41 gcd(x, 0) -> x 9.93/3.41 ) 9.93/3.41 9.93/3.41 Matrix Interpretation Processor: dim=2 9.93/3.41 9.93/3.41 interpretation: 9.93/3.41 [2 2] [2 0] 9.93/3.41 [?3](x0, x1) = [0 3]x0 + [2 0]x1, 9.93/3.41 9.93/3.41 [1 0] 9.93/3.41 [s](x0) = [2 3]x0, 9.93/3.41 9.93/3.41 [1 1] [1 0] [1 2] [0] 9.93/3.41 [?1](x0, x1, x2) = [0 1]x0 + [1 0]x1 + [0 0]x2 + [2], 9.93/3.41 9.93/3.41 [0] 9.93/3.41 [0] = [0], 9.93/3.41 9.93/3.41 [1 1] [1 3] [1 0] [0] 9.93/3.41 [?2](x0, x1, x2) = [0 1]x0 + [2 0]x1 + [0 0]x2 + [2], 9.93/3.41 9.93/3.41 [3 3] [3 3] [0] 9.93/3.41 [gcd](x0, x1) = [2 1]x0 + [0 1]x1 + [2], 9.93/3.41 9.93/3.41 [1 2] [2 0] 9.93/3.41 [tp2](x0, x1) = [2 1]x0 + [0 1]x1, 9.93/3.41 9.93/3.41 [2 2] 9.93/3.41 [iadd](x0) = [0 1]x0, 9.93/3.41 9.93/3.41 [1 1] [1 1] [1] 9.93/3.41 [add](x0, x1) = [2 1]x0 + [0 2]x1 + [0] 9.93/3.41 orientation: 9.93/3.41 [6 4] [2 6] [2] [1 2] [2 0] 9.93/3.41 iadd(add(x,y)) = [2 1]x + [0 2]y + [0] >= [2 1]x + [0 1]y = tp2(x,y) 9.93/3.41 9.93/3.41 [3 3] [3 3] [0] [1 3] [3 3] [0] 9.93/3.41 gcd(y,z) = [2 1]y + [0 1]z + [2] >= [2 0]y + [0 1]z + [2] = ?2(iadd(z),y,z) 9.93/3.41 9.93/3.41 [3 3] [3 4] [1 0] [0] [3 3] [3 3] [0] 9.93/3.41 ?2(tp2(x,y),y,z) = [2 1]x + [2 1]y + [0 0]z + [2] >= [2 1]x + [0 1]y + [2] = gcd(x,y) 9.93/3.41 9.93/3.41 [3 3] [0] 9.93/3.41 gcd(0(),x) = [0 1]x + [2] >= x = x 9.93/3.41 9.93/3.41 [3 3] [3 3] [0] [1 2] [3 3] [0] 9.93/3.41 gcd(z,y) = [0 1]y + [2 1]z + [2] >= [0 0]y + [1 1]z + [2] = ?1(iadd(z),z,y) 9.93/3.41 9.93/3.41 [3 3] [3 3] [1 0] [0] [3 3] [3 3] [0] 9.93/3.41 ?1(tp2(x,y),z,y) = [2 1]x + [0 1]y + [1 0]z + [2] >= [2 1]x + [0 1]y + [2] = gcd(x,y) 9.93/3.41 9.93/3.41 [2 2] [2 0] 9.93/3.41 iadd(y) = [0 1]y >= [0 1]y = tp2(0(),y) 9.93/3.41 9.93/3.41 [6 6] [6 6] 9.93/3.41 iadd(s(z)) = [2 3]z >= [2 3]z = ?3(iadd(z),z) 9.93/3.41 9.93/3.41 [6 6] [4 2] [2 0] [5 6] [2 0] 9.93/3.41 ?3(tp2(x,y),z) = [6 3]x + [0 3]y + [2 0]z >= [4 3]x + [0 1]y = tp2(s(x),y) 9.93/3.41 9.93/3.41 [3 3] [0] 9.93/3.41 gcd(x,0()) = [2 1]x + [2] >= x = x 9.93/3.41 problem: 9.93/3.41 gcd(y,z) -> ?2(iadd(z),y,z) 9.93/3.41 ?2(tp2(x,y),y,z) -> gcd(x,y) 9.93/3.41 gcd(0(),x) -> x 9.93/3.41 gcd(z,y) -> ?1(iadd(z),z,y) 9.93/3.41 ?1(tp2(x,y),z,y) -> gcd(x,y) 9.93/3.41 iadd(y) -> tp2(0(),y) 9.93/3.41 iadd(s(z)) -> ?3(iadd(z),z) 9.93/3.41 ?3(tp2(x,y),z) -> tp2(s(x),y) 9.93/3.41 gcd(x,0()) -> x 9.93/3.41 Matrix Interpretation Processor: dim=2 9.93/3.41 9.93/3.41 interpretation: 9.93/3.41 [2 0] [1 0] 9.93/3.41 [?3](x0, x1) = [0 3]x0 + [0 0]x1, 9.93/3.41 9.93/3.41 [2 0] 9.93/3.41 [s](x0) = [1 2]x0, 9.93/3.41 9.93/3.41 [2 2] [1 0] [1] 9.93/3.41 [?1](x0, x1, x2) = [0 2]x0 + [0 0]x1 + x2 + [0], 9.93/3.41 9.93/3.41 [0] 9.93/3.41 [0] = [0], 9.93/3.41 9.93/3.41 [2 2] [1 2] [1 0] [1] 9.93/3.41 [?2](x0, x1, x2) = [0 2]x0 + [0 1]x1 + [0 0]x2 + [0], 9.93/3.41 9.93/3.41 [3 2] [3 2] [1] 9.93/3.41 [gcd](x0, x1) = [0 1]x0 + [0 1]x1 + [0], 9.93/3.41 9.93/3.41 [1 0] [1 1] 9.93/3.41 [tp2](x0, x1) = [2 2]x0 + [0 0]x1, 9.93/3.41 9.93/3.41 [1 1] 9.93/3.41 [iadd](x0) = [0 0]x0 9.93/3.41 orientation: 9.93/3.41 [3 2] [3 2] [1] [1 2] [3 2] [1] 9.93/3.41 gcd(y,z) = [0 1]y + [0 1]z + [0] >= [0 1]y + [0 0]z + [0] = ?2(iadd(z),y,z) 9.93/3.41 9.93/3.41 [6 4] [3 4] [1 0] [1] [3 2] [3 2] [1] 9.93/3.41 ?2(tp2(x,y),y,z) = [4 4]x + [0 1]y + [0 0]z + [0] >= [0 1]x + [0 1]y + [0] = gcd(x,y) 9.93/3.41 9.93/3.41 [3 2] [1] 9.93/3.41 gcd(0(),x) = [0 1]x + [0] >= x = x 9.93/3.41 9.93/3.41 [3 2] [3 2] [1] [3 2] [1] 9.93/3.41 gcd(z,y) = [0 1]y + [0 1]z + [0] >= y + [0 0]z + [0] = ?1(iadd(z),z,y) 9.93/3.41 9.93/3.41 [6 4] [3 2] [1 0] [1] [3 2] [3 2] [1] 9.93/3.41 ?1(tp2(x,y),z,y) = [4 4]x + [0 1]y + [0 0]z + [0] >= [0 1]x + [0 1]y + [0] = gcd(x,y) 9.93/3.41 9.93/3.41 [1 1] [1 1] 9.93/3.41 iadd(y) = [0 0]y >= [0 0]y = tp2(0(),y) 9.93/3.41 9.93/3.41 [3 2] [3 2] 9.93/3.41 iadd(s(z)) = [0 0]z >= [0 0]z = ?3(iadd(z),z) 9.93/3.41 9.93/3.41 [2 0] [2 2] [1 0] [2 0] [1 1] 9.93/3.41 ?3(tp2(x,y),z) = [6 6]x + [0 0]y + [0 0]z >= [6 4]x + [0 0]y = tp2(s(x),y) 9.93/3.41 9.93/3.41 [3 2] [1] 9.93/3.41 gcd(x,0()) = [0 1]x + [0] >= x = x 9.93/3.41 problem: 9.93/3.41 gcd(y,z) -> ?2(iadd(z),y,z) 9.93/3.41 ?2(tp2(x,y),y,z) -> gcd(x,y) 9.93/3.41 gcd(z,y) -> ?1(iadd(z),z,y) 9.93/3.41 ?1(tp2(x,y),z,y) -> gcd(x,y) 9.93/3.41 iadd(y) -> tp2(0(),y) 9.93/3.41 iadd(s(z)) -> ?3(iadd(z),z) 9.93/3.41 ?3(tp2(x,y),z) -> tp2(s(x),y) 9.93/3.41 Unfolding Processor: 9.93/3.41 loop length: 3 9.93/3.41 terms: 9.93/3.41 gcd(0(),0()) 9.93/3.41 ?2(iadd(0()),0(),0()) 9.93/3.41 ?2(tp2(0(),0()),0(),0()) 9.93/3.42 context: [] 9.93/3.42 substitution: 9.93/3.42 9.93/3.42 Qed 9.93/3.42 9.93/3.43 EOF