[Termtools] SRS/Zantema/z090?
Aart Middeldorp
Aart.Middeldorp at uibk.ac.at
Mon Jun 11 17:32:18 CEST 2007
Dear all,
Concerning the termination proof for SRS/Zantema/z090 generated by
TTT2, we believe it is correct. Attached the generated proof with
some added comments (* ... *) which may help to understand it. The
key ingredient is a version of self-labeling in a DP setting. (This
technique preserves minimality of DP problems. So does usable rules
computation for SRSs. The latter is used in the proof but can be
avoided by changing the strategy.)
During our investigations of the proof, we learned that due to a
"miscommunication" in the TTT2 team, the strategy for TRSs is not
guaranteed to be correct. We use usable rules with projection as a
stand-alone processor. Since this may not preserve minimality, it
may be possible to construct a counterexample. (Maybe a nice task
for the AProVE team?)
Now what to do? Should TTT2 be removed from the TRS table since
correctness is not guaranteed? We wonder though what message that
conveys. Only three participants in the TRS category? AProVE against
a weak version of Jambox (due to unclear time limits?) and a tool
(NTI) that "only" aims to disprove termination?
> There's the analogy of not publishing the titles of papers
> that have been rejected from a conference/journal.
With the crucial difference that submission of papers is typically not
made public....
Consider MU-TERM for instance. We find the polynomial interpretations
with rational coefficients that it (quickly) generates very interesting.
Since the bug is due to narrowing, it is very easy to filter out wrong
proofs. Instead, MU-TERM is allowed to participate in the CSR category,
although it is pretty clear that it may produce incorrect proofs (but
not on the systems used for the competition): adding a full replacement
map to the TRS counterexample should do the trick.
Concerning time limits, presumably most of us tuned their tools to 60
seconds, because this was the announced time limit in an email of Hans
before the competition. Of course, as correctly observed by Claude,
exactly measuring time is tricky if not impossible due to parallellism
and multi-core hardware. Specifying a timeout range could work, if the
the actual time limit is passed to the tools.
That's all for now.
TTT2
-------------- next part --------------
Result for tool TTT2 on problem id: SRS/Zantema - z090
YES
Trs:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Comment:
We consider a overlapping trs.
DP:
{ b_dp=# u -> b_dp=# s,
b_dp=# u -> s_dp=#,
t_dp=# b s -> b_dp=#,
t_dp=# b s -> t_dp=# b,
t_dp=# b -> b_dp=# s,
t_dp=# b -> s_dp=#,
t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=#,
s_dp=# b s -> b_dp=# t,
s_dp=# b s -> t_dp=#,
s_dp=# b -> b_dp=# s s s,
s_dp=# b -> s_dp=# s s,
s_dp=# b -> s_dp=# s,
s_dp=# b -> s_dp=#,
s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=#}
Comment:
We consider a overlapping trs.
EDG:
(s_dp=# b -> s_dp=# s s,
s_dp=# b s -> b_dp=# t),
(s_dp=# b -> s_dp=# s s,
s_dp=# b s -> t_dp=#),
(s_dp=# b -> s_dp=# s s,
s_dp=# b -> b_dp=# s s s),
(s_dp=# b -> s_dp=# s s,
s_dp=# b -> s_dp=# s s),
(s_dp=# b -> s_dp=# s s,
s_dp=# b -> s_dp=# s),
(s_dp=# b -> s_dp=# s s,
s_dp=# b -> s_dp=#),
(s_dp=# b -> s_dp=# s s,
s_dp=# u -> s_dp=# s),
(s_dp=# b -> s_dp=# s s,
s_dp=# u -> s_dp=#),
(s_dp=# b -> s_dp=# s,
s_dp=# b s -> b_dp=# t),
(s_dp=# b -> s_dp=# s,
s_dp=# b s -> t_dp=#),
(s_dp=# b -> s_dp=# s,
s_dp=# b -> b_dp=# s s s),
(s_dp=# b -> s_dp=# s,
s_dp=# b -> s_dp=# s s),
(s_dp=# b -> s_dp=# s,
s_dp=# b -> s_dp=# s),
(s_dp=# b -> s_dp=# s,
s_dp=# b -> s_dp=#),
(s_dp=# b -> s_dp=# s,
s_dp=# u -> s_dp=# s),
(s_dp=# b -> s_dp=# s,
s_dp=# u -> s_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# b s -> b_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# b s -> t_dp=# b),
(t_dp=# s -> t_dp=# t,
t_dp=# b -> b_dp=# s),
(t_dp=# s -> t_dp=# t,
t_dp=# b -> s_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# u -> t_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=# t),
(t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> b_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> t_dp=# b),
(t_dp=# b s -> t_dp=# b,
t_dp=# b -> b_dp=# s),
(t_dp=# b s -> t_dp=# b,
t_dp=# b -> s_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# s -> t_dp=# t),
(t_dp=# b s -> t_dp=# b,
t_dp=# s -> t_dp=#),
(s_dp=# u -> s_dp=#,
s_dp=# b s -> b_dp=# t),
(s_dp=# u -> s_dp=#,
s_dp=# b s -> t_dp=#),
(s_dp=# u -> s_dp=#,
s_dp=# b -> b_dp=# s s s),
(s_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=# s s),
(s_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=# s),
(s_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=#),
(s_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=# s),
(s_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=#),
(s_dp=# b s -> t_dp=#,
t_dp=# b s -> b_dp=#),
(s_dp=# b s -> t_dp=#,
t_dp=# b s -> t_dp=# b),
(s_dp=# b s -> t_dp=#,
t_dp=# b -> b_dp=# s),
(s_dp=# b s -> t_dp=#,
t_dp=# b -> s_dp=#),
(s_dp=# b s -> t_dp=#,
t_dp=# u -> t_dp=#),
(s_dp=# b s -> t_dp=#,
t_dp=# s -> t_dp=# t),
(s_dp=# b s -> t_dp=#,
t_dp=# s -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# b s -> b_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# b s -> t_dp=# b),
(t_dp=# u -> t_dp=#,
t_dp=# b -> b_dp=# s),
(t_dp=# u -> t_dp=#,
t_dp=# b -> s_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t),
(t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=#),
(t_dp=# b s -> b_dp=#,
b_dp=# u -> b_dp=# s),
(t_dp=# b s -> b_dp=#,
b_dp=# u -> s_dp=#),
(b_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=#),
(b_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=# s),
(b_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=#),
(b_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=# s),
(b_dp=# u -> s_dp=#,
s_dp=# b -> s_dp=# s s),
(b_dp=# u -> s_dp=#,
s_dp=# b -> b_dp=# s s s),
(b_dp=# u -> s_dp=#,
s_dp=# b s -> t_dp=#),
(b_dp=# u -> s_dp=#,
s_dp=# b s -> b_dp=# t),
(t_dp=# b -> s_dp=#,
s_dp=# u -> s_dp=#),
(t_dp=# b -> s_dp=#,
s_dp=# u -> s_dp=# s),
(t_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=#),
(t_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=# s),
(t_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=# s s),
(t_dp=# b -> s_dp=#,
s_dp=# b -> b_dp=# s s s),
(t_dp=# b -> s_dp=#,
s_dp=# b s -> t_dp=#),
(t_dp=# b -> s_dp=#,
s_dp=# b s -> b_dp=# t),
(t_dp=# s -> t_dp=#,
t_dp=# s -> t_dp=#),
(t_dp=# s -> t_dp=#,
t_dp=# s -> t_dp=# t),
(t_dp=# s -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# s -> t_dp=#,
t_dp=# b -> s_dp=#),
(t_dp=# s -> t_dp=#,
t_dp=# b -> b_dp=# s),
(t_dp=# s -> t_dp=#,
t_dp=# b s -> t_dp=# b),
(t_dp=# s -> t_dp=#,
t_dp=# b s -> b_dp=#),
(s_dp=# b -> s_dp=#,
s_dp=# u -> s_dp=#),
(s_dp=# b -> s_dp=#,
s_dp=# u -> s_dp=# s),
(s_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=#),
(s_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=# s),
(s_dp=# b -> s_dp=#,
s_dp=# b -> s_dp=# s s),
(s_dp=# b -> s_dp=#,
s_dp=# b -> b_dp=# s s s),
(s_dp=# b -> s_dp=#,
s_dp=# b s -> t_dp=#),
(s_dp=# b -> s_dp=#,
s_dp=# b s -> b_dp=# t),
(b_dp=# u -> b_dp=# s,
b_dp=# u -> s_dp=#),
(b_dp=# u -> b_dp=# s,
b_dp=# u -> b_dp=# s),
(t_dp=# b -> b_dp=# s,
b_dp=# u -> s_dp=#),
(t_dp=# b -> b_dp=# s,
b_dp=# u -> b_dp=# s),
(s_dp=# b s -> b_dp=# t,
b_dp=# u -> s_dp=#),
(s_dp=# b s -> b_dp=# t,
b_dp=# u -> b_dp=# s),
(s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=#),
(s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=# s),
(s_dp=# u -> s_dp=# s,
s_dp=# b -> s_dp=#),
(s_dp=# u -> s_dp=# s,
s_dp=# b -> s_dp=# s),
(s_dp=# u -> s_dp=# s,
s_dp=# b -> s_dp=# s s),
(s_dp=# u -> s_dp=# s,
s_dp=# b -> b_dp=# s s s),
(s_dp=# u -> s_dp=# s,
s_dp=# b s -> t_dp=#),
(s_dp=# u -> s_dp=# s,
s_dp=# b s -> b_dp=# t),
(s_dp=# b -> b_dp=# s s s,
b_dp=# u -> s_dp=#),
(s_dp=# b -> b_dp=# s s s,
b_dp=# u -> b_dp=# s)
SCCS:
(* there is one SCC consisting of all DPs *)
SCC:
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* we count b symbols *)
Interpretation:
[u](x0) = 1x0,
[s](x0) = 1x0,
[b_dp=#](x0) = 1x0,
[t_dp=#](x0) = 1x0,
[s_dp=#](x0) = 1x0,
[b](x0) = 1x0 + 1,
[t](x0) = 1x0
Strict:
(* these are the remaining DPs *)
{ b_dp=# u -> b_dp=# s,
b_dp=# u -> s_dp=#,
t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=#,
s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=#}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# s -> t_dp=#,
t_dp=# b s -> t_dp=# b),
(t_dp=# s -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# s -> t_dp=#,
t_dp=# s -> t_dp=# t),
(t_dp=# s -> t_dp=#,
t_dp=# s -> t_dp=#),
(b_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=# s),
(b_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# b s -> t_dp=# b),
(t_dp=# s -> t_dp=# t,
t_dp=# u -> t_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=# t),
(t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=#),
(b_dp=# u -> b_dp=# s,
b_dp=# u -> b_dp=# s),
(b_dp=# u -> b_dp=# s,
b_dp=# u -> s_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# s -> t_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# s -> t_dp=# t),
(t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> t_dp=# b),
(s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=#),
(s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=# s),
(t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t),
(t_dp=# u -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# b s -> t_dp=# b),
(s_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=#),
(s_dp=# u -> s_dp=#,
s_dp=# u -> s_dp=# s)
SCCS:
(* we recompute the dependency graph, resulting in 3 new SCCs *)
SCC:
(* the first SCC consists of { b_dp=# u -> b_dp=# s } *)
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[s_dp=#](x0) = 1x0,
[b](x0) = 0,
[t](x0) = 0,
[u](x0) = 1x0 + 1,
[s](x0) = 0
Strict:
{}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Qed
SCC:
(* the second SCC consists of { t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=# } *)
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[t_dp=#](x0) = 1x0,
[b](x0) = 1,
[t](x0) = 1,
[u](x0) = 1x0,
[s](x0) = 1x0 + 1
Strict:
(* DP t_dp=# s -> t_dp=# is removed *)
{t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# s -> t_dp=# t,
t_dp=# b s -> t_dp=# b),
(t_dp=# s -> t_dp=# t,
t_dp=# u -> t_dp=#),
(t_dp=# s -> t_dp=# t,
t_dp=# s -> t_dp=# t),
(t_dp=# b s -> t_dp=# b,
t_dp=# s -> t_dp=# t),
(t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#),
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> t_dp=# b),
(t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t),
(t_dp=# u -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# b s -> t_dp=# b)
SCCS:
(* recomputing the dependency graph produces the SCC
{ t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#,
t_dp=# s -> t_dp=# t } *)
SCC:
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[t_dp=#](x0) = 1x0,
[b](x0) = 0,
[t](x0) = 0,
[u](x0) = 1x0,
[s](x0) = 1
Strict:
(* DP t_dp=# s -> t_dp=# t is removed *)
{t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> t_dp=# b),
(t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# u -> t_dp=#),
(t_dp=# u -> t_dp=#,
t_dp=# b s -> t_dp=# b)
SCCS:
(* recomputing the dependency graph produces the SCC
{ t_dp=# b s -> t_dp=# b,
t_dp=# u -> t_dp=# } *)
SCC:
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[t_dp=#](x0) = 1x0 + 1,
[b](x0) = 0,
[t](x0) = 1,
[u](x0) = 1x0 + 1,
[s](x0) = 0
Strict:
(* DP t_dp=# u -> t_dp=# is removed *)
{t_dp=# b s -> t_dp=# b}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# b s -> t_dp=# b,
t_dp=# b s -> t_dp=# b)
SCCS:
(* recomputing the dependency graph produces the one-rule SCC
{ t_dp=# b s -> t_dp=# b } *)
SCC:
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Self Labeling:
(* self-labeling produces 4 "dependency pairs" and 112 rules;
0 = b, 1 = t, 2 = u, 3 = s *)
Strict:
{t_dp=# a_fs=[0] b_fs=[3] s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[0] -> t_dp=# a_fs=[0] b_fs=[0]}
Weak:
{a_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> a_fs=[0] b_fs=[1] t_fs=[3],
a_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> a_fs=[0] b_fs=[1] t_fs=[2],
a_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> a_fs=[0] b_fs=[1] t_fs=[1],
a_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> a_fs=[0] b_fs=[1] t_fs=[0],
a_fs=[3] s_fs=[0] b_fs=[3] -> a_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
a_fs=[3] s_fs=[0] b_fs=[2] -> a_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
a_fs=[3] s_fs=[0] b_fs=[1] -> a_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
a_fs=[3] s_fs=[0] b_fs=[0] -> a_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
a_fs=[1] t_fs=[2] u_fs=[3] -> a_fs=[2] u_fs=[1] t_fs=[3],
a_fs=[1] t_fs=[2] u_fs=[2] -> a_fs=[2] u_fs=[1] t_fs=[2],
a_fs=[1] t_fs=[2] u_fs=[1] -> a_fs=[2] u_fs=[1] t_fs=[1],
a_fs=[1] t_fs=[2] u_fs=[0] -> a_fs=[2] u_fs=[1] t_fs=[0],
a_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> a_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
a_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> a_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
a_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> a_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
a_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> a_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
a_fs=[1] t_fs=[0] b_fs=[3] -> a_fs=[0] b_fs=[3] s_fs=[3],
a_fs=[1] t_fs=[0] b_fs=[2] -> a_fs=[0] b_fs=[3] s_fs=[2],
a_fs=[1] t_fs=[0] b_fs=[1] -> a_fs=[0] b_fs=[3] s_fs=[1],
a_fs=[1] t_fs=[0] b_fs=[0] -> a_fs=[0] b_fs=[3] s_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[0] b_fs=[1] t_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[0] b_fs=[1] t_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[0] b_fs=[1] t_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[0] b_fs=[1] t_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
b_fs=[2] u_fs=[3] -> b_fs=[3] s_fs=[3],
b_fs=[2] u_fs=[2] -> b_fs=[3] s_fs=[2],
b_fs=[2] u_fs=[1] -> b_fs=[3] s_fs=[1],
b_fs=[2] u_fs=[0] -> b_fs=[3] s_fs=[0],
b_fs=[1] t_fs=[2] u_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[3],
b_fs=[1] t_fs=[2] u_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[2],
b_fs=[1] t_fs=[2] u_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[1],
b_fs=[1] t_fs=[2] u_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[3] -> t_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[2] -> t_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[1] -> t_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[0] b_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[0] b_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[0] b_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[0] b_fs=[1] t_fs=[0],
t_fs=[3] s_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[0] -> t_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[2] u_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[3],
t_fs=[1] t_fs=[2] u_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[2],
t_fs=[1] t_fs=[2] u_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[1],
t_fs=[1] t_fs=[2] u_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[0],
u_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[0] b_fs=[1] t_fs=[3],
u_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[0] b_fs=[1] t_fs=[2],
u_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[0] b_fs=[1] t_fs=[1],
u_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[0] b_fs=[1] t_fs=[0],
u_fs=[3] s_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
u_fs=[3] s_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
u_fs=[3] s_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
u_fs=[3] s_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
u_fs=[1] t_fs=[2] u_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[3],
u_fs=[1] t_fs=[2] u_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[2],
u_fs=[1] t_fs=[2] u_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[1],
u_fs=[1] t_fs=[2] u_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[0] b_fs=[1] t_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[0] b_fs=[1] t_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[0] b_fs=[1] t_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[0] b_fs=[1] t_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
s_fs=[2] u_fs=[3] -> s_fs=[3] s_fs=[3],
s_fs=[2] u_fs=[2] -> s_fs=[3] s_fs=[2],
s_fs=[2] u_fs=[1] -> s_fs=[3] s_fs=[1],
s_fs=[2] u_fs=[0] -> s_fs=[3] s_fs=[0],
s_fs=[1] t_fs=[2] u_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[3],
s_fs=[1] t_fs=[2] u_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[2],
s_fs=[1] t_fs=[2] u_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[1],
s_fs=[1] t_fs=[2] u_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[0]}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[0] -> t_dp=# a_fs=[0] b_fs=[0]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[0] -> t_dp=# a_fs=[0] b_fs=[0]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[0] -> t_dp=# a_fs=[0] b_fs=[0]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3])
SCCS:
(* computing the dependency graph produces the SCC {
{t_dp=# a_fs=[0] b_fs=[3] s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]} *)
SCC:
UR:
(* only 84 rules are usable; for the experts: TTT2 assumes minimality
for DP problems and stand-alone UR computation without adding
projection rules is sound for SRSs *)
{b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[0] b_fs=[1] t_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[0] b_fs=[1] t_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[0] b_fs=[1] t_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[0] b_fs=[1] t_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
b_fs=[2] u_fs=[3] -> b_fs=[3] s_fs=[3],
b_fs=[2] u_fs=[2] -> b_fs=[3] s_fs=[2],
b_fs=[2] u_fs=[1] -> b_fs=[3] s_fs=[1],
b_fs=[2] u_fs=[0] -> b_fs=[3] s_fs=[0],
b_fs=[1] t_fs=[2] u_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[3],
b_fs=[1] t_fs=[2] u_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[2],
b_fs=[1] t_fs=[2] u_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[1],
b_fs=[1] t_fs=[2] u_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[3] -> t_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[2] -> t_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[1] -> t_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[0] b_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[0] b_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[0] b_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[0] b_fs=[1] t_fs=[0],
t_fs=[3] s_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[0] -> t_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[2] u_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[3],
t_fs=[1] t_fs=[2] u_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[2],
t_fs=[1] t_fs=[2] u_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[1],
t_fs=[1] t_fs=[2] u_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[0],
u_fs=[1] t_fs=[2] u_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[3],
u_fs=[1] t_fs=[2] u_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[2],
u_fs=[1] t_fs=[2] u_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[1],
u_fs=[1] t_fs=[2] u_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[0] b_fs=[1] t_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[0] b_fs=[1] t_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[0] b_fs=[1] t_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[0] b_fs=[1] t_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
s_fs=[2] u_fs=[3] -> s_fs=[3] s_fs=[3],
s_fs=[2] u_fs=[2] -> s_fs=[3] s_fs=[2],
s_fs=[2] u_fs=[1] -> s_fs=[3] s_fs=[1],
s_fs=[2] u_fs=[0] -> s_fs=[3] s_fs=[0],
s_fs=[1] t_fs=[2] u_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[3],
s_fs=[1] t_fs=[2] u_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[2],
s_fs=[1] t_fs=[2] u_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[1],
s_fs=[1] t_fs=[2] u_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[0]}
MATRIX:
(* we count u_fs=[3] symbols; wrong interpretation printed *)
Interpretation:
[b](x0) = 1x0 + 1,
[t](x0) = 1x0 + 1,
[u](x0) = 1x0 + 1,
[s](x0) = 1x0 + 1
Strict:
{t_dp=# a_fs=[0] b_fs=[3] s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3] s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]}
Weak:
(* we get rid of an additional 6 rules; 78 remaining *)
{b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[0] b_fs=[1] t_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[0] b_fs=[1] t_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[0] b_fs=[1] t_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[0] b_fs=[1] t_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
b_fs=[2] u_fs=[2] -> b_fs=[3] s_fs=[2],
b_fs=[2] u_fs=[1] -> b_fs=[3] s_fs=[1],
b_fs=[2] u_fs=[0] -> b_fs=[3] s_fs=[0],
b_fs=[1] t_fs=[2] u_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[2],
b_fs=[1] t_fs=[2] u_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[1],
b_fs=[1] t_fs=[2] u_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[3] -> t_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[2] -> t_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[1] -> t_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[0] b_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[0] b_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[0] b_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[0] b_fs=[1] t_fs=[0],
t_fs=[3] s_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[0] -> t_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[2] u_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[2],
t_fs=[1] t_fs=[2] u_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[1],
t_fs=[1] t_fs=[2] u_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[0],
u_fs=[1] t_fs=[2] u_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[2],
u_fs=[1] t_fs=[2] u_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[1],
u_fs=[1] t_fs=[2] u_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[0] b_fs=[1] t_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[0] b_fs=[1] t_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[0] b_fs=[1] t_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[0] b_fs=[1] t_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
s_fs=[2] u_fs=[2] -> s_fs=[3] s_fs=[2],
s_fs=[2] u_fs=[1] -> s_fs=[3] s_fs=[1],
s_fs=[2] u_fs=[0] -> s_fs=[3] s_fs=[0],
s_fs=[1] t_fs=[2] u_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[2],
s_fs=[1] t_fs=[2] u_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[1],
s_fs=[1] t_fs=[2] u_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[0]}
Comment:
We consider a overlapping trs.
EDG:
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[2] -> t_dp=# a_fs=[0] b_fs=[2]),
(t_dp=# a_fs=[0] b_fs=[3]
s_fs=[1] -> t_dp=# a_fs=[0] b_fs=[1],
t_dp=# a_fs=[0] b_fs=[3]
s_fs=[3] -> t_dp=# a_fs=[0] b_fs=[3])
SCCS:
(* recomputing the dependency graph has no effect *)
SCC:
(* we still have 3 strict pairs ... *)
UR:
(* and 78 weak rules *)
{b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[0] b_fs=[1] t_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[0] b_fs=[1] t_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[0] b_fs=[1] t_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[0] b_fs=[1] t_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
b_fs=[2] u_fs=[2] -> b_fs=[3] s_fs=[2],
b_fs=[2] u_fs=[1] -> b_fs=[3] s_fs=[1],
b_fs=[2] u_fs=[0] -> b_fs=[3] s_fs=[0],
b_fs=[1] t_fs=[2] u_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[2],
b_fs=[1] t_fs=[2] u_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[1],
b_fs=[1] t_fs=[2] u_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[3] -> t_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[2] -> t_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[1] -> t_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[0] b_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[0] b_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[0] b_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[0] b_fs=[1] t_fs=[0],
t_fs=[3] s_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[0] -> t_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[2] u_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[2],
t_fs=[1] t_fs=[2] u_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[1],
t_fs=[1] t_fs=[2] u_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[0],
u_fs=[1] t_fs=[2] u_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[2],
u_fs=[1] t_fs=[2] u_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[1],
u_fs=[1] t_fs=[2] u_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[0] b_fs=[1] t_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[0] b_fs=[1] t_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[0] b_fs=[1] t_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[0] b_fs=[1] t_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
s_fs=[2] u_fs=[2] -> s_fs=[3] s_fs=[2],
s_fs=[2] u_fs=[1] -> s_fs=[3] s_fs=[1],
s_fs=[2] u_fs=[0] -> s_fs=[3] s_fs=[0],
s_fs=[1] t_fs=[2] u_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[2],
s_fs=[1] t_fs=[2] u_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[1],
s_fs=[1] t_fs=[2] u_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[0]}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[u_fs=[2]](x0) = 1x0 + 1,
[s_fs=[2]](x0) = 1x0 + 1,
[b_fs=[1]](x0) = 1x0,
[t_fs=[1]](x0) = 1x0 + 1,
[u_fs=[1]](x0) = 1x0 + 1,
[s_fs=[1]](x0) = 1x0 + 1,
[a_fs=[0]](x0) = 1x0,
[b_fs=[0]](x0) = 0,
[t_fs=[0]](x0) = 1x0 + 1,
[u_fs=[0]](x0) = 1x0 + 1,
[s_fs=[0]](x0) = 1,
[b_fs=[3]](x0) = 1x0,
[t_fs=[3]](x0) = 0,
[s_fs=[3]](x0) = 1x0 + 1,
[t_dp=#](x0) = 1x0,
[b_fs=[2]](x0) = 1x0,
[t_fs=[2]](x0) = 1x0 + 1
Strict:
{}
Weak:
{b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[0] b_fs=[1] t_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[0] b_fs=[1] t_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[0] b_fs=[1] t_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[0] b_fs=[1] t_fs=[0],
b_fs=[3] s_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
b_fs=[3] s_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
b_fs=[3] s_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
b_fs=[3] s_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
b_fs=[2] u_fs=[2] -> b_fs=[3] s_fs=[2],
b_fs=[2] u_fs=[1] -> b_fs=[3] s_fs=[1],
b_fs=[2] u_fs=[0] -> b_fs=[3] s_fs=[0],
b_fs=[1] t_fs=[2] u_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[2],
b_fs=[1] t_fs=[2] u_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[1],
b_fs=[1] t_fs=[2] u_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> b_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
b_fs=[1] t_fs=[0] b_fs=[3] -> b_fs=[0] b_fs=[3] s_fs=[3],
b_fs=[1] t_fs=[0] b_fs=[2] -> b_fs=[0] b_fs=[3] s_fs=[2],
b_fs=[1] t_fs=[0] b_fs=[1] -> b_fs=[0] b_fs=[3] s_fs=[1],
b_fs=[1] t_fs=[0] b_fs=[0] -> b_fs=[0] b_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[3] -> t_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[2] -> t_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[1] -> t_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[0] b_fs=[1] t_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[0] b_fs=[1] t_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[0] b_fs=[1] t_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[0] b_fs=[1] t_fs=[0],
t_fs=[3] s_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
t_fs=[3] s_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
t_fs=[3] s_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
t_fs=[3] s_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
t_fs=[3] s_fs=[0] -> t_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[2] u_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[2],
t_fs=[1] t_fs=[2] u_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[1],
t_fs=[1] t_fs=[2] u_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> t_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
t_fs=[1] t_fs=[0] b_fs=[3] -> t_fs=[0] b_fs=[3] s_fs=[3],
t_fs=[1] t_fs=[0] b_fs=[2] -> t_fs=[0] b_fs=[3] s_fs=[2],
t_fs=[1] t_fs=[0] b_fs=[1] -> t_fs=[0] b_fs=[3] s_fs=[1],
t_fs=[1] t_fs=[0] b_fs=[0] -> t_fs=[0] b_fs=[3] s_fs=[0],
u_fs=[1] t_fs=[2] u_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[2],
u_fs=[1] t_fs=[2] u_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[1],
u_fs=[1] t_fs=[2] u_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> u_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
u_fs=[1] t_fs=[0] b_fs=[3] -> u_fs=[0] b_fs=[3] s_fs=[3],
u_fs=[1] t_fs=[0] b_fs=[2] -> u_fs=[0] b_fs=[3] s_fs=[2],
u_fs=[1] t_fs=[0] b_fs=[1] -> u_fs=[0] b_fs=[3] s_fs=[1],
u_fs=[1] t_fs=[0] b_fs=[0] -> u_fs=[0] b_fs=[3] s_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[0] b_fs=[1] t_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[0] b_fs=[1] t_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[0] b_fs=[1] t_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[0] b_fs=[1] t_fs=[0],
s_fs=[3] s_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[3],
s_fs=[3] s_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[2],
s_fs=[3] s_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[1],
s_fs=[3] s_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[3] s_fs=[3] s_fs=[0],
s_fs=[2] u_fs=[2] -> s_fs=[3] s_fs=[2],
s_fs=[2] u_fs=[1] -> s_fs=[3] s_fs=[1],
s_fs=[2] u_fs=[0] -> s_fs=[3] s_fs=[0],
s_fs=[1] t_fs=[2] u_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[2],
s_fs=[1] t_fs=[2] u_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[1],
s_fs=[1] t_fs=[2] u_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[3] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[2] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[1] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[3] s_fs=[0] -> s_fs=[2] u_fs=[1] t_fs=[0] b_fs=[0],
s_fs=[1] t_fs=[0] b_fs=[3] -> s_fs=[0] b_fs=[3] s_fs=[3],
s_fs=[1] t_fs=[0] b_fs=[2] -> s_fs=[0] b_fs=[3] s_fs=[2],
s_fs=[1] t_fs=[0] b_fs=[1] -> s_fs=[0] b_fs=[3] s_fs=[1],
s_fs=[1] t_fs=[0] b_fs=[0] -> s_fs=[0] b_fs=[3] s_fs=[0]}
Qed
(* finally we got rid of the second SCC *)
SCC:
(* the third SCC consists of { s_dp=# u -> s_dp=# s,
s_dp=# u -> s_dp=# } *)
UR:
(* all rules are usable *)
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
MATRIX:
(* 0/1 linear polynomial interpretation with implicit usable rules *)
Interpretation:
[b](x0) = 0,
[t](x0) = 0,
[u](x0) = 1,
[s](x0) = 0,
[b_dp=#](x0) = 1x0
Strict:
{}
Weak:
{ b u -> b s,
t b s -> u t b,
t b -> b s,
t u -> u t,
t s -> t t,
s b s -> b t,
s b -> b s s s,
s u -> s s}
Qed
More information about the Termtools
mailing list