Confluence Problems (Cops)

59 problems found.
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
  typo: corrected version of Cops #273
  oriented and modified version of
  \cite{DOS87}, Example B
  doi: 10.1007/3-540-19242-5_3
)
format:
properties:
solved by:

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
  inlined version of adaptation of Cops #292
  example 5.15
  Thomas Sternagel PhD Thesis, not yet published
)
format:
properties:
solved by:

550.trs

(CONDITIONTYPE ORIENTED)
(VAR)
(RULES
  f(b) -> f(a)
  b -> c
  a -> c | b == c
)
(COMMENT
  example 6.3
  Thomas Sternagel PhD Thesis, not yet published
)
format:
properties:
solved by:

547.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(x) -> a | x == a
  f(x) -> b | x == b
)
(COMMENT
  example 4.13
  Thomas Sternagel PhD Thesis, not yet published
)
format:
properties:
solved by:

546.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  g(x) -> g(x) | g(x) == f(a,b)
  g(x) -> f(x,x)
)
(COMMENT
  example 7.37
  Thomas Sternagel PhD Thesis, not yet published
)
format:
properties:
solved by:

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
  typo: corrected version of Cops #313
  \cite{N04}, System R_31, p. 140
  http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf
)
format:
properties:
solved by:

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
  typo: Corrected version of Cops #404
  [Nishida, Yanagisawa, and Gmeiner, IWC 2014, Example 8]
)
format:
properties:
solved by:

495.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  h(x) -> a
  g(x) -> x
  g(x) -> a | h(x) == b
  c -> c
)
(COMMENT Example 17 from 10.4230/LIPIcs.FSCD.2016.29)
format:
properties:
solved by:

494.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(a,x) -> a
  f(b,x) -> b
  g(a,x) -> c | f(x,a) == a
  g(x,a) -> d | f(x,b) == b
  c -> c
)
(COMMENT Example 16 from 10.4230/LIPIcs.FSCD.2016.29)
format:
properties:
solved by:

491.trs

(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(g(x)) -> b | x == a
  g(x) -> c | x == c
)
(COMMENT
  IWC 2015, Infeasible Conditional Critical Pairs
  motivating example
)
format:
properties:
solved by:

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 
  example 2
)
format:
properties:
solved by:

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 from http://www.trs.cm.is.nagoya-u.ac.jp/co3/index.html#NKYG15v1.2)
format:
properties:
solved by:

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:
solved by:

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:
solved by:

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:
solved by:

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:
solved by:

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:
solved by:

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:
solved by:

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
  [Nishida, Yanagisawa, and Gmeiner, IWC 2014, Example 9]
)
format:
properties:
solved by:

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
  [Nishida, Yanagisawa, and Gmeiner, IWC 2014, Example 8] with typo; fixed as Cops #522
)
format:
properties:
solved by:

403.trs

uploaded: 2014-07-08
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  e(0) -> true
  e(s(x)) -> true  | e(x) == false
  e(s(x)) -> false | e(x) == true
)
(COMMENT
  [Nishida, Yanagisawa, and Gmeiner, IWC 2014, Example 2]
)
format:
properties:
solved by:

387.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(g(x)) -> x | x == s(0)
  g(s(x)) -> g(x)
)
(COMMENT
  \cite{G14}, example 10
  PhD Thesis, not yet published
)
format:
properties:
solved by:

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
  \cite{G14}, example 43
  PhD Thesis, not yet published
)
format:
properties:
solved by:

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
  \cite{G14}, example 42
  PhD Thesis, not yet published
)
format:
properties:
solved by:

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
  \cite{G14}, example 40
  PhD Thesis, not yet published
)
format:
properties:
solved by:

380.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x y)
(RULES
  f(x) -> x | x == a
  g(x) -> h(x, x)
  h(x, y) -> i(x)
)
(COMMENT
  \cite{G14}, example 39
  PhD Thesis, not yet published
)
format:
properties:
solved by:

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
  \cite{G14}, example 34
  PhD Thesis, not yet published
)
format:
properties:
solved by:

376.trs

uploaded: 2014-04-15
(CONDITIONTYPE ORIENTED)
(VAR x)
(RULES
  f(x) -> x | x == a
  g(x) -> C | A == B
  A -> B
)
(COMMENT
  \cite{G14}, example 33
  PhD Thesis, not yet published
)
format:
properties:
solved by:
PREV « 1 2 » NEXT order: desc asc