(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
NUMERAL(0) → 0
BIT0(0) → 0
SUC(NUMERAL(n)) → NUMERAL(SUC(n))
SUC(0) → BIT1(0)
SUC(BIT0(n)) → BIT1(n)
SUC(BIT1(n)) → BIT0(SUC(n))
PRE(NUMERAL(n)) → NUMERAL(PRE(n))
PRE(0) → 0
PRE(BIT0(n)) → if(eq(n, 0), 0, BIT1(PRE(n)))
PRE(BIT1(n)) → BIT0(n)
plus(NUMERAL(m), NUMERAL(n)) → NUMERAL(plus(m, n))
plus(0, 0) → 0
plus(0, BIT0(n)) → BIT0(n)
plus(0, BIT1(n)) → BIT1(n)
plus(BIT0(n), 0) → BIT0(n)
plus(BIT1(n), 0) → BIT1(n)
plus(BIT0(m), BIT0(n)) → BIT0(plus(m, n))
plus(BIT0(m), BIT1(n)) → BIT1(plus(m, n))
plus(BIT1(m), BIT0(n)) → BIT1(plus(m, n))
plus(BIT1(m), BIT1(n)) → BIT0(SUC(plus(m, n)))
mult(NUMERAL(m), NUMERAL(n)) → NUMERAL(mult(m, n))
mult(0, 0) → 0
mult(0, BIT0(n)) → 0
mult(0, BIT1(n)) → 0
mult(BIT0(n), 0) → 0
mult(BIT1(n), 0) → 0
mult(BIT0(m), BIT0(n)) → BIT0(BIT0(mult(m, n)))
mult(BIT0(m), BIT1(n)) → plus(BIT0(m), BIT0(BIT0(mult(m, n))))
mult(BIT1(m), BIT0(n)) → plus(BIT0(n), BIT0(BIT0(mult(m, n))))
mult(BIT1(m), BIT1(n)) → plus(plus(BIT1(m), BIT0(n)), BIT0(BIT0(mult(m, n))))
exp(NUMERAL(m), NUMERAL(n)) → NUMERAL(exp(m, n))
exp(0, 0) → BIT1(0)
exp(BIT0(m), 0) → BIT1(0)
exp(BIT1(m), 0) → BIT1(0)
exp(0, BIT0(n)) → mult(exp(0, n), exp(0, n))
exp(BIT0(m), BIT0(n)) → mult(exp(BIT0(m), n), exp(BIT0(m), n))
exp(BIT1(m), BIT0(n)) → mult(exp(BIT1(m), n), exp(BIT1(m), n))
exp(0, BIT1(n)) → 0
exp(BIT0(m), BIT1(n)) → mult(mult(BIT0(m), exp(BIT0(m), n)), exp(BIT0(m), n))
exp(BIT1(m), BIT1(n)) → mult(mult(BIT1(m), exp(BIT1(m), n)), exp(BIT1(m), n))
EVEN(NUMERAL(n)) → EVEN(n)
EVEN(0) → T
EVEN(BIT0(n)) → T
EVEN(BIT1(n)) → F
ODD(NUMERAL(n)) → ODD(n)
ODD(0) → F
ODD(BIT0(n)) → F
ODD(BIT1(n)) → T
eq(NUMERAL(m), NUMERAL(n)) → eq(m, n)
eq(0, 0) → T
eq(BIT0(n), 0) → eq(n, 0)
eq(BIT1(n), 0) → F
eq(0, BIT0(n)) → eq(0, n)
eq(0, BIT1(n)) → F
eq(BIT0(m), BIT0(n)) → eq(m, n)
eq(BIT0(m), BIT1(n)) → F
eq(BIT1(m), BIT0(n)) → F
eq(BIT1(m), BIT1(n)) → eq(m, n)
le(NUMERAL(m), NUMERAL(n)) → le(m, n)
le(0, 0) → T
le(BIT0(n), 0) → le(n, 0)
le(BIT1(n), 0) → F
le(0, BIT0(n)) → T
le(0, BIT1(n)) → T
le(BIT0(m), BIT0(n)) → le(m, n)
le(BIT0(m), BIT1(n)) → le(m, n)
le(BIT1(m), BIT0(n)) → lt(m, n)
le(BIT1(m), BIT1(n)) → le(m, n)
lt(NUMERAL(m), NUMERAL(n)) → lt(m, n)
lt(0, 0) → F
lt(BIT0(n), 0) → F
lt(BIT1(n), 0) → F
lt(0, BIT0(n)) → lt(0, n)
lt(0, BIT1(n)) → T
lt(BIT0(m), BIT0(n)) → lt(m, n)
lt(BIT0(m), BIT1(n)) → le(m, n)
lt(BIT1(m), BIT0(n)) → lt(m, n)
lt(BIT1(m), BIT1(n)) → lt(m, n)
ge(NUMERAL(n), NUMERAL(m)) → ge(n, m)
ge(0, 0) → T
ge(0, BIT0(n)) → ge(0, n)
ge(0, BIT1(n)) → F
ge(BIT0(n), 0) → T
ge(BIT1(n), 0) → T
ge(BIT0(n), BIT0(m)) → ge(n, m)
ge(BIT1(n), BIT0(m)) → ge(n, m)
ge(BIT0(n), BIT1(m)) → gt(n, m)
ge(BIT1(n), BIT1(m)) → ge(n, m)
gt(NUMERAL(n), NUMERAL(m)) → gt(n, m)
gt(0, 0) → F
gt(0, BIT0(n)) → F
gt(0, BIT1(n)) → F
gt(BIT0(n), 0) → gt(n, 0)
gt(BIT1(n), 0) → T
gt(BIT0(n), BIT0(m)) → gt(n, m)
gt(BIT1(n), BIT0(m)) → ge(n, m)
gt(BIT0(n), BIT1(m)) → gt(n, m)
gt(BIT1(n), BIT1(m)) → gt(n, m)
minus(NUMERAL(m), NUMERAL(n)) → NUMERAL(minus(m, n))
minus(0, 0) → 0
minus(0, BIT0(n)) → 0
minus(0, BIT1(n)) → 0
minus(BIT0(n), 0) → BIT0(n)
minus(BIT1(n), 0) → BIT1(n)
minus(BIT0(m), BIT0(n)) → BIT0(minus(m, n))
minus(BIT0(m), BIT1(n)) → PRE(BIT0(minus(m, n)))
minus(BIT1(m), BIT0(n)) → if(le(n, m), BIT1(minus(m, n)), 0)
minus(BIT1(m), BIT1(n)) → BIT0(minus(m, n))
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
exp2 > mult2 > plus2 > [0, T] > [NUMERAL1, BIT01, SUC1, BIT11, if3, F, ge2, gt2]
EVEN1 > [0, T] > [NUMERAL1, BIT01, SUC1, BIT11, if3, F, ge2, gt2]
ODD1 > [0, T] > [NUMERAL1, BIT01, SUC1, BIT11, if3, F, ge2, gt2]
minus2 > PRE1 > eq2 > [0, T] > [NUMERAL1, BIT01, SUC1, BIT11, if3, F, ge2, gt2]
minus2 > [le2, lt2] > [0, T] > [NUMERAL1, BIT01, SUC1, BIT11, if3, F, ge2, gt2]
Status:
NUMERAL1: [1]
0: multiset
BIT01: [1]
SUC1: [1]
BIT11: [1]
PRE1: multiset
if3: [2,1,3]
eq2: [2,1]
plus2: [1,2]
mult2: [1,2]
exp2: [2,1]
EVEN1: multiset
T: multiset
F: multiset
ODD1: multiset
le2: [1,2]
lt2: [1,2]
ge2: multiset
gt2: multiset
minus2: [1,2]
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
NUMERAL(0) → 0
BIT0(0) → 0
SUC(BIT0(n)) → BIT1(n)
PRE(NUMERAL(n)) → NUMERAL(PRE(n))
PRE(0) → 0
PRE(BIT0(n)) → if(eq(n, 0), 0, BIT1(PRE(n)))
PRE(BIT1(n)) → BIT0(n)
plus(NUMERAL(m), NUMERAL(n)) → NUMERAL(plus(m, n))
plus(0, 0) → 0
plus(0, BIT0(n)) → BIT0(n)
plus(0, BIT1(n)) → BIT1(n)
plus(BIT0(n), 0) → BIT0(n)
plus(BIT1(n), 0) → BIT1(n)
plus(BIT0(m), BIT0(n)) → BIT0(plus(m, n))
plus(BIT0(m), BIT1(n)) → BIT1(plus(m, n))
plus(BIT1(m), BIT0(n)) → BIT1(plus(m, n))
plus(BIT1(m), BIT1(n)) → BIT0(SUC(plus(m, n)))
mult(NUMERAL(m), NUMERAL(n)) → NUMERAL(mult(m, n))
mult(0, 0) → 0
mult(0, BIT0(n)) → 0
mult(0, BIT1(n)) → 0
mult(BIT0(n), 0) → 0
mult(BIT1(n), 0) → 0
mult(BIT0(m), BIT0(n)) → BIT0(BIT0(mult(m, n)))
mult(BIT0(m), BIT1(n)) → plus(BIT0(m), BIT0(BIT0(mult(m, n))))
mult(BIT1(m), BIT0(n)) → plus(BIT0(n), BIT0(BIT0(mult(m, n))))
mult(BIT1(m), BIT1(n)) → plus(plus(BIT1(m), BIT0(n)), BIT0(BIT0(mult(m, n))))
exp(NUMERAL(m), NUMERAL(n)) → NUMERAL(exp(m, n))
exp(0, 0) → BIT1(0)
exp(BIT0(m), 0) → BIT1(0)
exp(BIT1(m), 0) → BIT1(0)
exp(0, BIT0(n)) → mult(exp(0, n), exp(0, n))
exp(BIT0(m), BIT0(n)) → mult(exp(BIT0(m), n), exp(BIT0(m), n))
exp(BIT1(m), BIT0(n)) → mult(exp(BIT1(m), n), exp(BIT1(m), n))
exp(0, BIT1(n)) → 0
exp(BIT0(m), BIT1(n)) → mult(mult(BIT0(m), exp(BIT0(m), n)), exp(BIT0(m), n))
exp(BIT1(m), BIT1(n)) → mult(mult(BIT1(m), exp(BIT1(m), n)), exp(BIT1(m), n))
EVEN(NUMERAL(n)) → EVEN(n)
EVEN(0) → T
EVEN(BIT0(n)) → T
EVEN(BIT1(n)) → F
ODD(NUMERAL(n)) → ODD(n)
ODD(0) → F
ODD(BIT0(n)) → F
ODD(BIT1(n)) → T
eq(NUMERAL(m), NUMERAL(n)) → eq(m, n)
eq(0, 0) → T
eq(BIT0(n), 0) → eq(n, 0)
eq(BIT1(n), 0) → F
eq(0, BIT0(n)) → eq(0, n)
eq(0, BIT1(n)) → F
eq(BIT0(m), BIT0(n)) → eq(m, n)
eq(BIT0(m), BIT1(n)) → F
eq(BIT1(m), BIT0(n)) → F
eq(BIT1(m), BIT1(n)) → eq(m, n)
le(NUMERAL(m), NUMERAL(n)) → le(m, n)
le(0, 0) → T
le(BIT0(n), 0) → le(n, 0)
le(BIT1(n), 0) → F
le(0, BIT0(n)) → T
le(0, BIT1(n)) → T
le(BIT0(m), BIT0(n)) → le(m, n)
le(BIT0(m), BIT1(n)) → le(m, n)
le(BIT1(m), BIT0(n)) → lt(m, n)
le(BIT1(m), BIT1(n)) → le(m, n)
lt(NUMERAL(m), NUMERAL(n)) → lt(m, n)
lt(0, 0) → F
lt(BIT0(n), 0) → F
lt(BIT1(n), 0) → F
lt(0, BIT0(n)) → lt(0, n)
lt(0, BIT1(n)) → T
lt(BIT0(m), BIT0(n)) → lt(m, n)
lt(BIT0(m), BIT1(n)) → le(m, n)
lt(BIT1(m), BIT0(n)) → lt(m, n)
lt(BIT1(m), BIT1(n)) → lt(m, n)
ge(NUMERAL(n), NUMERAL(m)) → ge(n, m)
ge(0, 0) → T
ge(0, BIT0(n)) → ge(0, n)
ge(0, BIT1(n)) → F
ge(BIT0(n), 0) → T
ge(BIT1(n), 0) → T
ge(BIT0(n), BIT0(m)) → ge(n, m)
ge(BIT1(n), BIT0(m)) → ge(n, m)
ge(BIT0(n), BIT1(m)) → gt(n, m)
ge(BIT1(n), BIT1(m)) → ge(n, m)
gt(NUMERAL(n), NUMERAL(m)) → gt(n, m)
gt(0, 0) → F
gt(0, BIT0(n)) → F
gt(0, BIT1(n)) → F
gt(BIT0(n), 0) → gt(n, 0)
gt(BIT1(n), 0) → T
gt(BIT0(n), BIT0(m)) → gt(n, m)
gt(BIT1(n), BIT0(m)) → ge(n, m)
gt(BIT0(n), BIT1(m)) → gt(n, m)
gt(BIT1(n), BIT1(m)) → gt(n, m)
minus(NUMERAL(m), NUMERAL(n)) → NUMERAL(minus(m, n))
minus(0, 0) → 0
minus(0, BIT0(n)) → 0
minus(0, BIT1(n)) → 0
minus(BIT0(n), 0) → BIT0(n)
minus(BIT1(n), 0) → BIT1(n)
minus(BIT0(m), BIT0(n)) → BIT0(minus(m, n))
minus(BIT0(m), BIT1(n)) → PRE(BIT0(minus(m, n)))
minus(BIT1(m), BIT0(n)) → if(le(n, m), BIT1(minus(m, n)), 0)
minus(BIT1(m), BIT1(n)) → BIT0(minus(m, n))
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
SUC(NUMERAL(n)) → NUMERAL(SUC(n))
SUC(0) → BIT1(0)
SUC(BIT1(n)) → BIT0(SUC(n))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
SUC1 > BIT01 > BIT11 > 0 > NUMERAL1
and weight map:
0=1
SUC_1=2
NUMERAL_1=1
BIT1_1=2
BIT0_1=2
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
SUC(NUMERAL(n)) → NUMERAL(SUC(n))
SUC(0) → BIT1(0)
SUC(BIT1(n)) → BIT0(SUC(n))
(4) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(5) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(6) YES