Certification Problem

Input (COPS 493)

The rewrite relation of the following conditional TRS is considered.

eq(0,0)	→	true
eq(s(x),0)	→	false
eq(0,s(y))	→	false
eq(s(x),s(y))	→	eq(x,y)
lte(0,y)	→	true
lte(s(x),0)	→	false
lte(s(x),s(y))	→	lte(x,y)
m(0,s(y))	→	0
m(x,0)	→	x
m(s(x),s(y))	→	m(x,y)
mod(0,y)	→	0
mod(s(x),0)	→	0
mod(s(x),s(y))	→	mod(m(x,y),s(y))	\| lte(y,x) ≈ true
mod(s(x),s(y))	→	s(x)	\| lte(y,x) ≈ false
filter(n,r,nil)	→	nil
filter(n,r,cons(x,xs))	→	cons(x,filter(n,r,xs))	\| mod(x,n) ≈ r', eq(r,r') ≈ true
filter(n,r,cons(x,xs))	→	filter(n,r,xs)	\| mod(x,n) ≈ r', eq(r,r') ≈ false

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

1 Inlining of Conditions

Inlining of conditions results in the following transformed CTRS having the same multistep rewrite relation.

eq(0,0)	→	true
eq(s(x),0)	→	false
eq(0,s(y))	→	false
eq(s(x),s(y))	→	eq(x,y)
lte(0,y)	→	true
lte(s(x),0)	→	false
lte(s(x),s(y))	→	lte(x,y)
m(0,s(y))	→	0
m(x,0)	→	x
m(s(x),s(y))	→	m(x,y)
mod(0,y)	→	0
mod(s(x),0)	→	0
mod(s(x),s(y))	→	mod(m(x,y),s(y))	\| lte(y,x) ≈ true
mod(s(x),s(y))	→	s(x)	\| lte(y,x) ≈ false
filter(n,r,nil)	→	nil
filter(n,r,cons(x,xs))	→	cons(x,filter(n,r,xs))	\| eq(r,mod(x,n)) ≈ true
filter(n,r,cons(x,xs))	→	filter(n,r,xs)	\| eq(r,mod(x,n)) ≈ false

1.1 Almost-orthogonal modulo infeasibility

The given (extended) properly oriented, right-stable, oriented 3-CTRS is almost-orthogonal modulo infeasibility, since all its conditional critical pairs are infeasible.

The 1^st CCP contains the condition lte(z',y') ≈ false from the first rule and the condition lte(z',y') ≈ true from the second rule.
1.1.1 Equal Left-Hand Sides
There are two conditions with left-hand side lte(z',y') and respective right-hand sides false and true.
1.1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 2^nd CCP contains the condition lte(z',y') ≈ true from the first rule and the condition lte(z',y') ≈ false from the second rule.
1.1.2 Equal Left-Hand Sides
There are two conditions with left-hand side lte(z',y') and respective right-hand sides true and false.
1.1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 3^rd CCP contains the condition eq($1,mod($2,z')) ≈ false from the first rule and the condition eq($1,mod($2,z')) ≈ true from the second rule.
1.1.3 Equal Left-Hand Sides
There are two conditions with left-hand side eq($1,mod($2,z')) and respective right-hand sides false and true.
1.1.3.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 4^th CCP contains the condition eq($1,mod($2,z')) ≈ true from the first rule and the condition eq($1,mod($2,z')) ≈ false from the second rule.
1.1.4 Equal Left-Hand Sides
There are two conditions with left-hand side eq($1,mod($2,z')) and respective right-hand sides true and false.
1.1.4.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.

Certification Problem

Input (COPS 493)

Property / Task

Answer / Result

Proof (by ConCon @ CoCo 2020)

1 Inlining of Conditions

1.1 Almost-orthogonal modulo infeasibility

1.1.1 Equal Left-Hand Sides

1.1.1.1 Non-joinability by TCAP

1.1.2 Equal Left-Hand Sides

1.1.2.1 Non-joinability by TCAP

1.1.3 Equal Left-Hand Sides

1.1.3.1 Non-joinability by TCAP

1.1.4 Equal Left-Hand Sides

1.1.4.1 Non-joinability by TCAP