The
1st
CCP contains
the conditions y' ≈ x, x' ≈ x, y' ≈ y, h(x') ≈ y1.2.1 Infeasible Subset
We only consider the following subset of conditions:
| y' |
→ |
x |
(7) |
| x' |
→ |
x |
(8) |
| y' |
→ |
y |
(9) |
|
h(x') |
→ |
y |
(10) |
1.2.1.1 Infeasible Compound Conditions
We collect the conditions in the fresh compound-symbol
conds.
1.2.1.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.2.1.1.1.1 Non-reachability via Ordered Completion
We extend the signature by the binary function symbol
eq
and the two constants
true
and
false
and apply ordered completion using the TRS extended by two equality rules as set of initial equations
E0, in order to disprove the equality
true = false.
1.2.1.1.1.1.1 Disproof via Ordered Completion
Ordered completion is applied to E0, resulting
in a ground complete system. The goal equation is ground and
its two terms have different normal forms in the resulting system.
Ordered completion results in the TRS R
and the set of equations E
|
g(x) |
= |
g(y') |
(12) |
|
f(x,y') |
= |
f(x',y) |
(13) |
|
eq(conds(y',x',y',h(x')),conds(x,x,y,y)) |
= |
false |
(14) |
|
f(x',x'') |
= |
g(x) |
(15) |
|
f(y',h(y'')) |
= |
g(y) |
(16) |
It is proven that E0 is equivalent to (E,R),
and (E,R) is ground complete with respect to the following reduction order:
Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(conds) |
= |
3 |
|
weight(conds) |
= |
0 |
|
|
|
| prec(g) |
= |
4 |
|
weight(g) |
= |
1 |
|
|
|
| prec(h) |
= |
5 |
|
weight(h) |
= |
1 |
|
|
|
| prec(false) |
= |
6 |
|
weight(false) |
= |
1 |
|
|
|
| prec(f) |
= |
7 |
|
weight(f) |
= |
0 |
|
|
|
| prec(true) |
= |
8 |
|
weight(true) |
= |
2 |
|
|
|
| prec(eq) |
= |
9 |
|
weight(eq) |
= |
1 |
|
|
|
An ordered completion run on E0 using the given reduction order
produces the system (E,R).
The run consists of the following steps:
-
deduce
f(x,y')←g(x1673)→f(x',y)
-
deduce
g(x)←f(x1682,x1683)→g(y')
-
orient left-to-right
eq(x,x)→true
The
2nd
CCP contains
the conditions x' ≈ y, h(z') ≈ y, x' ≈ x, z' ≈ x1.2.2 Infeasible Subset
We only consider the following subset of conditions:
| x' |
→ |
y |
(17) |
|
h(z') |
→ |
y |
(18) |
| x' |
→ |
x |
(8) |
| z' |
→ |
x |
(19) |
1.2.2.1 Infeasible Compound Conditions
We collect the conditions in the fresh compound-symbol
conds.
1.2.2.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.2.2.1.1.1 Non-reachability via Ordered Completion
We extend the signature by the binary function symbol
eq
and the two constants
true
and
false
and apply ordered completion using the TRS extended by two equality rules as set of initial equations
E0, in order to disprove the equality
true = false.
1.2.2.1.1.1.1 Disproof via Ordered Completion
Ordered completion is applied to E0, resulting
in a ground complete system. The goal equation is ground and
its two terms have different normal forms in the resulting system.
Ordered completion results in the TRS R
and the set of equations E
|
g(x) |
= |
g(x') |
(20) |
|
f(x,x') |
= |
f(z',y) |
(21) |
|
eq(conds(x',h(z'),x',z'),conds(y,y,x,x)) |
= |
false |
(22) |
|
f(x',x'') |
= |
g(x) |
(15) |
|
f(y',h(y'')) |
= |
g(y) |
(16) |
It is proven that E0 is equivalent to (E,R),
and (E,R) is ground complete with respect to the following reduction order:
Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(conds) |
= |
3 |
|
weight(conds) |
= |
0 |
|
|
|
| prec(g) |
= |
4 |
|
weight(g) |
= |
1 |
|
|
|
| prec(h) |
= |
5 |
|
weight(h) |
= |
1 |
|
|
|
| prec(false) |
= |
6 |
|
weight(false) |
= |
1 |
|
|
|
| prec(f) |
= |
7 |
|
weight(f) |
= |
0 |
|
|
|
| prec(true) |
= |
8 |
|
weight(true) |
= |
2 |
|
|
|
| prec(eq) |
= |
9 |
|
weight(eq) |
= |
1 |
|
|
|
An ordered completion run on E0 using the given reduction order
produces the system (E,R).
The run consists of the following steps:
-
deduce
f(x,x')←g(x1674)→f(z',y)
-
deduce
g(x)←f(x1683,x1684)→g(x')
-
orient left-to-right
eq(x,x)→true