Certification Problem

Input (COPS 272)

The rewrite relation of the following conditional TRS is considered.

lte(0,n)	→	true
lte(s(m),0)	→	false
lte(s(m),s(n))	→	lte(m,n)
insert(nil,m)	→	cons(m,nil)
insert(cons(n,l),m)	→	cons(m,cons(n,l))	\| lte(m,n) ≈ true
insert(cons(n,l),m)	→	cons(n,insert(l,m))	\| lte(m,n) ≈ false
ordered(nil)	→	true
ordered(cons(m,nil))	→	true
ordered(cons(m,cons(n,l)))	→	ordered(cons(n,l))	\| lte(m,n) ≈ true
ordered(cons(m,cons(n,l)))	→	false	\| lte(m,n) ≈ false

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 condition lte(y',z') ≈ false from the first rule and the condition lte(y',z') ≈ true from the second rule.
1.1 Equal Left-Hand Sides
There are two conditions with left-hand side lte(y',z') 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 lte(y',z') ≈ true from the first rule and the condition lte(y',z') ≈ false from the second rule.
1.2 Equal Left-Hand Sides
There are two conditions with left-hand side lte(y',z') and respective right-hand sides true and false.
1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 3^rd CCP contains the condition lte(y',z') ≈ false from the first rule and the condition lte(y',z') ≈ true from the second rule.
1.3 Equal Left-Hand Sides
There are two conditions with left-hand side lte(y',z') and respective right-hand sides false and true.
1.3.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The 4^th CCP contains the condition lte(y',z') ≈ true from the first rule and the condition lte(y',z') ≈ false from the second rule.
1.4 Equal Left-Hand Sides
There are two conditions with left-hand side lte(y',z') and respective right-hand sides true and false.
1.4.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.

Certification Problem

Input (COPS 272)

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

1.3 Equal Left-Hand Sides

1.3.1 Non-joinability by TCAP

1.4 Equal Left-Hand Sides

1.4.1 Non-joinability by TCAP