Certification Problem

Input (COPS 288)

The rewrite relation of the following conditional TRS is considered.

pin(a)	→	pout(b)
pin(b)	→	pout(c)
tc(x)	→	x
tc(x)	→	y	\| pin(x) ≈ pout(z), tc(z) ≈ y

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.

pin(a)	→	pout(b)
pin(b)	→	pout(c)
tc(x)	→	x
tc(x)	→	tc(z)	\| pin(x) ≈ pout(z)

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 pin(x') ≈ pout(z) from the first rule and no conditions from the second rule.

1.1.1 Infeasible Equation

The equation is infeasible.

1.1.1.1 Non-reachability

We show non-reachability w.r.t. the underlying TRS.

1.1.1.1.1 Non-reachability via Exact Tree Automata Completion

Considering the signature {pin/1, z/0, tc/1, a/0, b/0, pout/1, c/0} as well as the fresh constant * the following tree automaton (overapproximating the set of ancestors of the ground instances of the target term) certifies non-reachability.

final states:

{1}

transitions:

tc(5)	→	5
z	→	4
tc(0)	→	0
pin(6)	→	0
pin(3)	→	5
pin(6)	→	4
tc(4)	→	7
pout(2)	→	1
tc(6)	→	6
a	→	4
tc(4)	→	4
tc(3)	→	3
b	→	3
tc(7)	→	7
pout(4)	→	4
tc(1)	→	1
tc(2)	→	2
pin(4)	→	4
b	→	4
z	→	2
a	→	6
tc(4)	→	2
c	→	4
pin(3)	→	4

States correspond to terms as follows:

0	↦	pin(a)
1	↦	pout(z)
2	↦	z
3	↦	b
4	↦	*
5	↦	pin(b)
6	↦	a
7	↦	tc(*)

The 2^nd CCP contains no conditions from the first rule and the condition pin(x') ≈ pout(z) from the second rule.

1.1.2 Infeasible Equation

The equation is infeasible.

1.1.2.1 Non-reachability

We show non-reachability w.r.t. the underlying TRS.

1.1.2.1.1 Non-reachability via Exact Tree Automata Completion

final states:

{1}

transitions:

tc(5)	→	5
z	→	4
tc(0)	→	0
pin(6)	→	0
pin(3)	→	5
pin(6)	→	4
tc(4)	→	7
pout(2)	→	1
tc(6)	→	6
a	→	4
tc(4)	→	4
tc(3)	→	3
b	→	3
tc(7)	→	7
pout(4)	→	4
tc(1)	→	1
tc(2)	→	2
pin(4)	→	4
b	→	4
z	→	2
a	→	6
tc(4)	→	2
c	→	4
pin(3)	→	4

States correspond to terms as follows:

0	↦	pin(a)
1	↦	pout(z)
2	↦	z
3	↦	b
4	↦	*
5	↦	pin(b)
6	↦	a
7	↦	tc(*)