Certification Problem

Input (COPS 335)

The rewrite relation of the following conditional TRS is considered.

lt(x,0)	→	false
lt(0,s(x))	→	true
lt(s(x),s(y))	→	lt(x,y)
m(0,s(y))	→	0
m(x,0)	→	x
m(s(x),s(y))	→	m(x,y)
div(0,s(x))	→	pair(0,0)
div(s(x),s(y))	→	pair(0,s(x))	\| lt(x,y) ≈ true
div(s(x),s(y))	→	pair(s(q),r)	\| lt(x,y) ≈ false, div(m(x,y),s(y)) ≈ pair(q,r)

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by ConCon @ CoCo 2020)

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 conditions lt($1,$2) ≈ false, div(m($1,$2),s($2)) ≈ pair(z,x') from the first rule and the condition lt($1,$2) ≈ true from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side lt($1,$2) and respective right-hand sides false and true.
1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 2^nd CCP contains the condition lt($1,$2) ≈ true from the first rule and the conditions lt($1,$2) ≈ false, div(m($1,$2),s($2)) ≈ pair(y',z') from the second rule.
1.2 Equal Left-Hand Sides
There are two conditions with left-hand side lt($1,$2) and respective right-hand sides true and false.
1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.

Certification Problem

Input (COPS 335)

Property / Task

Answer / Result

Proof (by ConCon @ CoCo 2020)

1 Almost-orthogonal modulo infeasibility

1.1 Equal Left-Hand Sides

1.1.1 Non-joinability by TCAP

1.2 Equal Left-Hand Sides

1.2.1 Non-joinability by TCAP