Confluence Problems (Cops)

59 problems matched.
PREV « 1 2 » NEXT order: desc asc

553.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  c -> k(f(a))
  c -> k(g(b))
  h(x) -> k(x)
  h(f(a)) -> c
  a -> b
  f(x) -> g(x) | h(f(x)) == k(g(b))
)
(COMMENT
doi:10.1007/3-540-19242-5_3
[49] Example B as join CTRS; correction of Cops #273
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

552.trs

(CONDITIONTYPE ORIENTED)
(VAR x y xs)
(RULES
  le(x,0) -> false
  le(0,s(y)) -> true
  le(s(x),s(y)) -> le(x, y)
  min(cons(x,nil)) -> x
  min(cons(x,xs)) -> x | le(x,min(xs)) == true
  min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false
)
(COMMENT
[121] Example 5.15; inlined version of Cops #551
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

546.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  g(x) -> g(x) | g(x) == f(a,b)
  g(x) -> f(x,x)
)
(COMMENT
[121] Example 7.37
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

523.trs

(CONDITIONTYPE ORIENTED)
(VAR x xd xm xy y)
(RULES
  add(0, y) -> y
  add(s(x), y) -> s(add(x, y))
  mul(0, y) -> 0
  mul(x, 0) -> 0
  mul(s(x), s(y)) -> s(add(mul(x, s(y)), y))
  leq(0, 0) -> T
  leq(s(x), 0) -> F
  leq(0, s(y)) -> T
  leq(s(x), s(y)) -> leq(x, y)
  n(xd, xm, xy) -> add(xd, add(mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))), xm), mul(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), xy))) | leq(0, xd) == T, leq(xd, s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))) == T, leq(0, xm) == T, leq(xm, s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) == T 
)
(COMMENT
[63] TRS R_31, p. 140; correction of Cops #313
http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

522.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  e(0) -> true
  e(s(x)) -> true  | o(x) == true
  e(s(x)) -> false | e(x) == true
  o(0) -> false
  o(s(x)) -> true  | e(x) == true
  o(s(x)) -> false | o(x) == true
)
(COMMENT
[79] Example 8; correction of Cops #404
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

489.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
 even(0) -> true
 even(s(x)) -> true | odd(x) == true
 even(s(x)) -> false | even(x) == true
 odd(0) -> false
 odd(s(x)) -> true | even(x) == true
 odd(s(x)) -> false | odd(x) == true
)
(COMMENT
doi:10.4230/LIPIcs.RTA.2015.223 
[89] Example 2
submitted by: Thomas Sternagel
)
format:
properties:
CoCo:

440.trs

(CONDITIONTYPE ORIENTED)
(VAR x y z)
(RULES
  f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) == c(a(b))
  f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) == c(a(a(b)))
  h(b) -> b
  h(a(a(x))) -> a(b) | h(x) == b
)
(COMMENT
Example 1 in extended version of [92]
)
format:
properties:
CoCo:

411.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(x) | a == d
 f(x,y) -> h(x) | b == d
 g(s(x)) -> x
 h(s(x)) -> x
 a -> d
 b -> d
 e -> e
)
format:
properties:
CoCo:

410.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(x) | a == d
 f(x,y) -> h(x) | b == d
 g(s(x)) -> x
 h(s(x)) -> x
 a -> d
 b -> d
)
format:
properties:
CoCo:

409.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(s(x)) | c(g(x)) == c(a)
 f(x,y) -> h(s(x)) | c(h(x)) == c(a)
 g(s(x)) -> x
 h(s(x)) -> x
 b -> b
)
format:
properties:
CoCo:

408.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(s(x)) | c(g(x)) == c(a)
 f(x,y) -> h(s(x)) | c(h(x)) == c(a)
 g(s(x)) -> x
 h(s(x)) -> x
)
format:
properties:
CoCo:

407.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(x) | c(g(x)) == c(a)
 f(x,y) -> h(x) | c(h(x)) == c(a)
 g(s(x)) -> x
 h(s(x)) -> x
 b -> b
)
format:
properties:
CoCo:

406.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
 f(x,y) -> g(x) | c(g(x)) == c(a)
 f(x,y) -> h(x) | c(h(x)) == c(a)
 g(s(x)) -> x
 h(s(x)) -> x
)
format:
properties:
CoCo:

405.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x y l)
(RULES
  dot(x,dot(y,l)) -> dot(y,dot(x,l)) | les(x,y) == true
  les(0,0) -> false
  les(0,s(0)) -> true
  les(0,s(s(x))) -> les(0,s(x))
  les(s(0),0) -> false
  les(s(s(x)),0) -> les(s(x),0)
  les(s(x),s(y)) -> les(x,y)
)
(COMMENT
[79] Example 9
)
format:
properties:
CoCo:

404.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  e(0) -> true
  e(s(x)) -> true  | o(x) == true
  e(s(x)) -> false | e(x) == true
  o(0) -> true
  o(s(x)) -> true  | e(x) == true
  o(s(x)) -> false | o(x) == true
)
(COMMENT
[79] Example 8 with typo; corrected as Cops #522
)
format:
properties:
CoCo:

387.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(g(x)) -> x | x == s(0)
  g(s(x)) -> g(x)
)
(COMMENT
[75] Example 10
submitted by: Thomas Sternagel and Aart Middeldorp
)
format:
properties:
CoCo:

384.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(x) -> A | s(x) == t
  f(x) -> B | s(x) == t
  s(a) -> t
  s(b) -> t
  a -> c
  b -> c
  g(x, x) -> h(x, x)
)
(COMMENT
[75] Example 43
submitted by: Thomas Sternagel and Aart Middeldorp
)
format:
properties:
CoCo:

383.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  a -> c
  a -> d
  b -> c
  b -> d
  f(x) -> x | x == c
  g(x, x) -> h(x, x)
  h(x, f(x)) -> x
)
(COMMENT
[75] Example 42
submitted by: Thomas Sternagel and Aart Middeldorp
)
format:
properties:
CoCo:

381.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  a -> c
  a -> d
  b -> c
  b -> d
  c -> e
  c -> k
  d -> k
  f(x) -> x | x == e
  g(x, x) -> C | A == B
  h(x) -> i(x, x)
)
(COMMENT
[75] Example 40
submitted by: Thomas Sternagel and Aart Middeldorp
)
format:
properties:
CoCo:

377.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  a -> c
  a -> d
  b -> c
  b -> d
  g(x, x) -> h(x, x)
  f(x) -> x | x == c
)
(COMMENT
[75] Example 34
submitted by: Thomas Sternagel and Aart Middeldorp
)
format:
properties:
CoCo:
PREV « 1 2 » NEXT order: desc asc