Confluence Problems (Cops)

765 problems found.
PREV « 1 2 3 4 10 20 26 » NEXT order: desc asc

765.trs

(VAR x y z)
(RULES
   xor(x,0) -> x
   xor(0,x) -> x
   xor(x,x) -> 0
   and(x,0) -> 0
   and(0,x) -> 0
   and(x,1) -> x
   and(1,x) -> x
   and(x,x) -> x
   xor(xor(x,y),z) -> xor(x,xor(y,z))
   xor(x,xor(y,z)) -> xor(y,xor(x,z))
   xor(x,y) -> xor(y,x)
   xor(x,xor(x,y)) -> y
   and(and(x,y),z) -> and(x,and(y,z))
   and(x,and(y,z)) -> and(y,and(x,z))
   and(x,y) -> and(y,x)
   and(x,and(x,y)) -> and(x,y)
   and(x,xor(y,z)) -> xor(and(x,y),xor(x,z))
   and(xor(x,y),z) -> xor(and(x,z),and(y,z))
)
(COMMENT
[113] Example 4.15; correction of Cops #536
submitted by: Takahito Aoto
)
format:
properties:
CoCo:

764.trs

(FUN
  f : (o -> o -> o) -> o
  a : o
  b : o
  c : o
  d : o
)
(VAR
  y : o
  x : o
  F : o -> o
)
(RULES
  f (\x y. F x) -> b,
  b -> f (\x y. a),
  b -> c,
  f (\x y. a) -> d
)
(COMMENT
[130] Example 7.16
submitted by: Julian Nagele
)
format:
properties:
CoCo:

763.trs

(VAR x)
(RULES
  f(f(x)) -> f(g(f(x),f(x)))
)
(COMMENT
[130] Example 4.24
submitted by: Julian Nagele
)
format:
properties:
CoCo:

762.trs

(VAR x)
(RULES
  a -> b
  f(a,b) -> f(a,a)
  f(b,a) -> f(a,a)
  f(a,a) -> c
  g(x) -> f(x,x)
)
(COMMENT
doi:10.23638/LMCS-13(2:4)2017
[131] Example 5.11
submitted by: Julian Nagele
)
format:
properties:
CoCo:

761.trs

(VAR )
(RULES
  a -> b
  a -> d
  b -> a
  c -> a
  c -> b
)
(COMMENT
doi:10.23638/LMCS-13(2:4)2017
[131] Example 5.2
submitted by: Julian Nagele
)
format:
properties:
CoCo:

760.trs

(VAR x)
(RULES
  f(x) -> f(f(x))
  g(x) -> f(x)
  f(x) -> g(x)
)
(COMMENT
[130] Example 3.29
submitted by: Julian Nagele
)
format:
properties:
CoCo:

759.trs

(FUN
  abs : (value -> term) -> value
  emb : value -> term
  app : term -> term -> term
)
(VAR
  x : value
  M : value -> term
  V : value
  N : term
  L : term
)
(RULES
  app (emb (abs (\x. M x))) (emb V) -> M V,
  app (app (emb (abs \x. M x)) N) L -> app (emb (abs \x.app (M x) L)) N,
  app (emb V) (app (emb (abs \x. M x)) N) -> app (emb (abs \x. app (emb V) (M x))) N
)
(COMMENT
doi:10.1007/978-3-642-54830-7_7
[135] Definition 1
submitted by: Vincent van Oostrom
)
format:
properties:
CoCo:

758.trs

(VAR
  d: data
  X: proc 
  Y: proc 
  Z: proc 
  E: data 
  P: data -> proc 
  Q: data -> proc 
)
(FUN
  xplus : proc -> proc -> proc
  xtimes : proc -> proc -> proc
  delta : proc
  sigma : (data -> proc) -> proc
)
(RULES
  xplus(X,X) -> X,
  xtimes(xplus(X,Y),Z) -> xplus(xtimes(X,Z),xtimes(Y,Z)),
  xtimes(xtimes(X,Y),Z) -> xtimes(X,xtimes(Y,Z)),
  xplus(X,delta) -> X,
  xtimes(delta,X) -> delta,
  sigma((\d.X)) -> X,
  xplus(sigma((\d.(P d))),(P E)) -> sigma((\d.(P d))),
  sigma((\d.xplus((P d),(Q d)))) -> xplus(sigma((\d.(P d))),sigma((\d.(Q d)))),
  xtimes(sigma((\d.(P d))),X) -> sigma((\d.xtimes((P d),X)))
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

757.trs

(VAR
  X: nat 
  Y: nat 
  P: nat -> bool
  n: nat
  z: natvar
)
(FUN
  0 : nat
  s : nat -> nat
  err : nat
  pre : nat -> nat
  id : nat -> nat
  add : nat -> nat -> nat
  eq : nat -> natp
  true : bool
  false : bool
  fn : (natvar -> bool) -> natp
  nul : nat -> bool
  at : natp -> nat -> bool
  v : natvar -> nat
)
(RULES
  nul(0) -> true,
  nul(s(X)) -> false,
  nul(err) -> false,
  pre(0) -> err,
  pre(s(X)) -> X,
  id(X) -> X,
  eq(0) -> fn (\z.nul (v z)),
  eq(s(X)) -> fn (\z.at (eq X) (pre (v z))),
  at(fn (\z.P (v z)),n) -> P n
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

756.trs

(VAR
  x: nat 
  n: var
  y: nat 
  U: nat 
  F: nat -> nat -> nat 
  z1: nat
  z2: nat
)
(FUN
  0 : nat
  s : nat -> nat
  xplus : nat -> nat -> nat
  xtimes : nat -> nat -> nat
  rec : nat -> nat -> (nat -> nat -> nat) -> nat
  v : var -> nat
)
(RULES
  xplus(x,0) -> x,
  xplus(x,s(y)) -> s(xplus(x,y)),
  rec(0,U,\z1 z2.F z1 z2) -> U,
  rec(s(v n),U,\z1 z2.F z1 z2) -> F(v n, rec(x,U,\z1 z2.F z1 z2)),
  xtimes(x,y) -> rec(y,0,(\z1.(\z2.xplus(x,z2))))
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

755.trs

(VAR
  F: N -> N 
  X: N 
  Y: N 
  Z: N 
  x: VN
  v: VN -> N
)
(FUN
  o : N
  s : N -> N
  fun : (VN -> N) -> N -> N -> N
  dom : N -> N -> N -> N
  eval : N -> N -> N
)
(RULES
  eval(fun(\x.F (v x),X,Y),Z) -> F(dom(X,Y,Z)),
  dom(s(X),s(Y),s(Z)) -> s(dom(X,Y,Z)),
  dom(o,s(Y),s(Z)) -> s(dom(o,Y,Z)),
  dom(X,Y,o) -> X,
  dom(o,o,Z) -> o
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

754.trs

(VAR
  x: var
  y: var
  F: var -> real 
  G: var -> real 
  M: real -> real
  N: real
)
(FUN
  0 : real
  1 : real
  sin : real -> real
  cos : real -> real
  ln : real -> real
  der : realfun -> realfun
  fn : (var -> real) -> realfun
  evalv : realfun -> var -> real
  eval : realfun -> real -> real
  v : var -> real
)
(RULES
  (der(fn(\x.v y ))) -> fn(\x.(0)),
  (der(fn(\x.v x ))) -> fn(\x.(1)),
  evalv(fn(\x.F x), y) -> F y,
  (der(fn(\x.(sin(v x))))) -> fn(\x.(cos(v x))),
  eval(fn(\x.M (v x)), N) -> M N
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

753.trs

(FUN
  case : SAB -> (A -> C) -> (B -> C) -> C
  inl : A -> SAB
  inr : B -> SAB
  f: A
  a: A
  b: A
)
(VAR
  x: A
  y: B
  X: A
  Y: B
  Z: SAB
  F: A -> C
  G: B -> C
  H: SAB -> C
)
(RULES
  case(inl(X), \x.F x , \y.G y ) -> F X ,
  case(inr(Y), \x.F x , \y.G y ) -> G Y,
  case(Z,\x.H (inl x), \y.H (inr y)) -> H Z,
  f -> a,
  f -> b
)
(COMMENT
doi:10.1007/3-540-58233-9_14
[134] Section 6.3 (variant)
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

752.trs

(FUN
  app : arrAB -> A -> B
  lam : (vA -> B) -> arrAB
  case : SAB -> (A -> C) -> (B -> C) -> C
  inl : A -> SAB
  inr : B -> SAB
  piA : PAB -> A
  piB : PAB -> B
  pair : A -> B -> PAB
  var : vA -> A
)
(VAR
  M: A -> B
  N: A
  L: arrAB
  x: vA
  y: B
  X: A
  Y: B
  Z: SAB
  F: A -> C
  G: B -> C
  H: SAB -> C
  M1 : A
  N1 : B
  M2 : PAB
  x0: A
)
(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L,
  piA(pair(M1,N1)) -> M1,
  piB(pair(M1,N1)) -> N1,
  case(inl(X), \x0.F x0 , \y.G y ) -> F X ,
  case(inr(Y), \x0.F x0 , \y.G y ) -> G Y 
)
(COMMENT
doi:10.1007/3-540-56939-1_109
[131] Section 3.3 (subsystem)
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

751.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBG : BGaBGb -> BGa -> BGb
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
)
(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  x1: BGa
  L: BGa
  P: BGaBGb
  C: BGa -> BGb
  Q: a -> BGb
  R: a
)
(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBG(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBG(S1, x1)) -> S1,
  let(L, \x. appBG(P, (banga x))) -> appBG(P, L),
  let(banga(R), \x.Q x) -> Q R,
  let(L, \x.C (banga x)) -> C L
)
(COMMENT
doi:10.1007/11805618_13
[132] Remark 2
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

750.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBG : BGaBGb -> BGa -> BGb
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
)
(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  x1: BGa
  L: BGa
  P: BGaBGb
  C: BGa -> BGb
  Q: a -> BGb
  R: a
)
(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBG(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBG(S1, x1)) -> S1,
  let(banga(R), \x.Q x) -> Q R,
  let(L, \x.C (banga x)) -> C L
)
(COMMENT
doi:10.1007/11805618_13
[132] Section 3.2 without commuting conversions
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

749.trs

(FUN
  abs : (a -> b) -> ab
  app : ab -> a -> b
  absBG : (BGa -> BGb) -> BGaBGb
  appBGaBGb : BGaBGb -> BGa -> BGb
  appBGbBGc : BGbBGc -> BGb -> BGc
  banga : a -> BGa
  let : BGa -> (a -> BGb) -> BGb
  letbc : BGb -> (b -> BGc) -> BGc
  letBGaBGb : BGa -> (a -> BGaBGb) -> BGaBGb
  letac : BGa -> (a -> BGc) -> BGc
)
(VAR
  M: a -> b
  N: a
  S: ab
  x: a
  M1: BGa -> BGb
  N1: BGa
  S1: BGaBGb
  S2: BGbBGc
  x1: BGa
  L: BGa
  C: BGa -> BGb
  Q: a -> BGb
  P: BGa -> a -> BGb
  K: b -> BGc
  y: b
  bc : BGc
)
(RULES
  app(abs(\x.M x), N) -> M N,
  abs(\x.app(S, x)) -> S,
  appBGaBGb(absBG(\x1.M1 x1), N1) -> M1 N1,
  absBG(\x1.appBGaBGb(S1, x1)) -> S1,
  let(banga(N), \x.Q x) -> Q N,
  let(L, \x.C (banga x)) -> C L,
  letbc(let(L,\x.Q x), \y.K y) -> letac(L, \x.letbc(Q x,\y.K y)),
  appBGbBGc(S2,let(L,\x.Q x)) -> letac(L, \x.appBGbBGc(S2, Q x))
)
(COMMENT
doi:10.1007/11805618_13
[132] Section 3.2 with (com2) and (com4)
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

748.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
  pia : prodab -> a
  pib : prodab -> b
  pair : a -> b -> prodab
)
(VAR
  x : Va
  M : a -> b
  N : a
  L : arrab
  M1 : a
  N1 : b
  M2 : prodab
)
(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L,
  pia(pair(M1,N1)) -> M1,
  pib(pair(M1,N1)) -> N1
)
(COMMENT
simply-typed lambda calculus with binary products in the style of [137,138]
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

747.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
)
(VAR
  x : Va
  M : a -> b
  N : a
  L : arrab
)
(RULES
  app(lam(\x.M (var x)), N) -> M N,
  lam(\x.app(L, (var x))) -> L
)
(COMMENT
simply-typed lambda calculus with beta/eta in the style of [137,138]
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

746.trs

(FUN
  app : arrab -> a -> b
  lam : (Va -> b) -> arrab
  var : Va -> a
)
(VAR
  x : Va
  M : a -> b
  N : a
)
(RULES
  app(lam(\x.M (var x)), N) -> M N
)
(COMMENT
simply-typed lambda calculus in the style of [137,138]
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

745.trs

(FUN
  c : v -> a
  d : v -> a
  f : (v -> b) -> b
  0 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  f(\x.M (c(x))) -> 0,
  f(\x.M (d(x))) -> 0
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

744.trs

(FUN
  c : v -> a
  d : v -> a
  f : (v -> b) -> b
  0 : b
  1 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  f(\x.M (c(x))) -> 1,
  f(\x.M (d(x))) -> 0
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

743.trs

(FUN
  c : v -> a
  g : b -> b
  0 : b
  1 : b
)
(VAR
  x : v
  M : a -> b
)
(RULES
  g(M(c(x))) -> 1,
  g(0) -> 0
)
(COMMENT
submitted by: Makoto Hamana
)
format:
properties:
CoCo:

742.trs

(VAR
  F: o -> o 
)
(FUN
  f : o -> o
  a : o
)
(RULES
  f(F(a)) -> a
)
(COMMENT
submitted by: anonymous
)
format:
properties:
CoCo:

741.trs

(VAR x)
(RULES
  if(true,a,x) -> a
  if(true,b,x) -> b
  if(true,g(a),x) -> g(a)
  if(true,g(b),x) -> g(b)
  if(false,x,a) -> a
  if(false,x,b) -> b
  if(false,x,g(a)) -> g(a)
  if(false,x,g(b)) -> g(b)
  g(a) -> g(g(a))
  g(b) -> a
  f(a,b) -> b
  f(g(g(a)),x) -> b
)
(COMMENT
handcrafted "UNC & ~NFP"
submitted by: Franziska Rapp
)
format:
properties:
CoCo:

739.trs

(VAR x)
(RULES
  a -> a
  g(g(a)) -> b
  g(g(x)) -> g(g(g(b)))
)
(COMMENT
generated by FORT "UN & ~UNC"
submitted by: Franziska Rapp
)
format:
properties:
CoCo:

738.trs

(VAR x)
(RULES
  a -> a
  f(b,a) -> f(a,b)
  f(x,a) -> b
)
(COMMENT
generated by FORT "UN & ~NFP"
submitted by: Franziska Rapp
)
format:
properties:
CoCo:
PREV « 1 2 3 4 10 20 26 » NEXT order: desc asc