(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
neg(0) → 0
neg(neg(x)) → x
plus(x, plus(y, z)) → plus(plus(x, y), z)
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(plus(x, 1), neg(1)) → x
plus(x, neg(plus(y, 1))) → plus(plus(x, neg(y)), neg(1))
plus(0, x) → x
plus(neg(1), 1) → 0
plus(neg(plus(x, 1)), 1) → neg(x)
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, 0) → 0
mult(x, 1) → x
mult(x, neg(y)) → mult(neg(x), y)
mult(x, plus(y, z)) → plus(mult(x, y), mult(x, z))
The set Q consists of the following terms:
neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
neg(
x1) =
x1
0 =
0
plus(
x1,
x2) =
plus(
x1,
x2)
1 =
1
mult(
x1,
x2) =
mult(
x1,
x2)
Recursive path order with status [RPO].
Quasi-Precedence:
mult2 > [0, plus2, 1]
Status:
0: multiset
plus2: [2,1]
1: multiset
mult2: [2,1]
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
plus(x, plus(y, z)) → plus(plus(x, y), z)
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(plus(x, 1), neg(1)) → x
plus(x, neg(plus(y, 1))) → plus(plus(x, neg(y)), neg(1))
plus(0, x) → x
plus(neg(1), 1) → 0
plus(neg(plus(x, 1)), 1) → neg(x)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, plus(y, z)) → plus(mult(x, y), mult(x, z))
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
neg(0) → 0
neg(neg(x)) → x
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → mult(neg(x), y)
The set Q consists of the following terms:
neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 1
POL(mult(x1, x2)) = 2·x1 + 2·x2
POL(neg(x1)) = 1 + x1
POL(plus(x1, x2)) = x1 + x2
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
neg(0) → 0
neg(neg(x)) → x
plus(neg(x), neg(y)) → neg(plus(x, y))
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
mult(x, neg(y)) → mult(neg(x), y)
The set Q consists of the following terms:
neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(mult(x1, x2)) = x1 + 2·x2
POL(neg(x1)) = 1 + x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
mult(x, neg(y)) → mult(neg(x), y)
(6) Obligation:
Q restricted rewrite system:
R is empty.
The set Q consists of the following terms:
neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))
(7) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) YES