* Step 1: Sum WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
- Signature:
{ 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
- Signature:
{ [0]
= S(0())
e2(a,b,res,False()) = [1] res + [3]
> [0]
= False()
e2(a,b,res,True()) = [1] res + [8]
> [1] res + [0]
= e3(a,b,res,True())
e4(a,b,res,False()) = [1] res + [5]
> [0]
= False()
e4(a,b,res,True()) = [1] res + [10]
> [5]
= True()
help1(0()) = [1]
> [0]
= False()
help1(S(0())) = [1]
> [0]
= False()
l13(x,y,res,tmp,True(),t) = [2] t + [2] tmp + [1] y + [6]
> [1] y + [4]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,True(),t) = [1] res + [1] y + [6]
> [1] y + [4]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [4]
> [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [2] mtmp + [2] res + [2] tmp + [1] x + [1] y + [5]
> [2] mtmp + [1] res + [1] tmp + [1] x + [1] y + [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [2] mtmp + [2] res + [2] tmp + [1] x + [1] y + [15]
> [1] res + [0]
= res
l5(x,y,res,tmp,mtmp,False()) = [1] res + [1] x + [1] y + [5]
> [1] res + [1] x + [1] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] res + [1] x + [1] y + [10]
> [0]
= 0()
l8(res,y,res',True(),mtmp,t) = [1] res + [1] res' + [1] y + [5]
> [1] res + [0]
= res
m2(a,b,res,False()) = [4] res + [2]
> [1] res + [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [4] res + [2]
> [0]
= False()
m2(S(0()),b,res,True()) = [4] res + [2]
> [0]
= False()
m3(0(),b,res,t) = [5]
> [0]
= False()
m3(S(0()),b,res,t) = [5]
> [0]
= False()
Following rules are (at-least) weakly oriented:
<(x,0()) = [5]
>= [0]
= False()
<(0(),S(y)) = [5]
>= [5]
= True()
<(S(x),S(y)) = [5]
>= [5]
= <(x,y)
bool2Nat(False()) = [0]
>= [0]
= 0()
e1(a,b,res,t) = [1] res + [0]
>= [1] res + [8]
= e2(a,b,res,<(a,b))
e3(a,b,res,t) = [1] res + [0]
>= [1] res + [10]
= e4(a,b,res,<(b,a))
e5(a,b,res,t) = [0]
>= [5]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [5]
= l1(x,y,0(),False(),False(),False())
help1(S(S(x))) = [1]
>= [5]
= True()
l1(x,y,res,tmp,mtmp,t) = [3] mtmp + [2] res + [4] tmp + [1] x + [1] y + [5]
>= [2] mtmp + [2] res + [2] tmp + [1] x + [1] y + [5]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] res + [3] tmp + [1] y + [4]
>= [1] res + [2] tmp + [1] y + [5]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] res + [2] tmp + [1] y + [0]
>= [1] res + [1] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] res + [2] tmp + [1] y + [5]
>= [1] res + [2] tmp + [1] y + [10]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] res + [2] t + [2] tmp + [1] y + [0]
>= [2] t + [2] tmp + [1] y + [1]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [2] t + [2] tmp + [1] y + [1]
>= [1] y + [4]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l14(x,y,res,tmp,mtmp,t) = [1] res + [1] t + [1] y + [0]
>= [1] res + [1] y + [1]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1] res + [1] y + [1]
>= [1] y + [4]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l3(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] res + [1] t + [1] tmp + [1] x + [1] y + [0]
>= [1] x + [1] y + [1]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [5] res + [1] x + [1] x' + [1]
>= [1] res + [1] x + [1] x' + [5]
= l5(x',x,res,tmp,mtmp,False())
l6(x,y,res,tmp,mtmp,t) = [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] res + [1] x + [1] y + [0]
>= [1] res + [1] x + [1] y + [0]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(x,y,res,False(),mtmp,t) = [1] res + [1] x + [1] y + [0]
>= [1] res + [1] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [7] res + [1]
>= [4] res + [2]
= m2(a,x,res,False())
m2(S(S(x)),b,res,True()) = [4] res + [2]
>= [5]
= True()
m3(S(S(x)),b,res,t) = [5]
>= [5]
= True()
m4(S(x'),S(x),res,t) = [1] res + [0]
>= [0]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [2] b + [1] res + [0]
>= [1] res + [0]
= res
monus(a,b) = [0]
>= [1]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
bool2Nat(False()) -> 0()
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(S(S(x)),b,res,True()) -> True()
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
help1(0()) -> False()
help1(S(0())) -> False()
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
- Signature:
{ [1]
= e4(a,b,res,<(b,a))
e8(a,b,res,t) = [1] res + [2] t + [1]
> [1] res + [0]
= res
l10(x,y,res,tmp,mtmp,t) = [4] tmp + [1] x + [2] y + [4]
> [2] y + [1]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] y + [1]
> [2] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] y + [1]
> [2] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l15(x,y,res,tmp,False(),t) = [2] y + [3]
> [2] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
m2(S(S(x)),b,res,True()) = [3] res + [1]
> [0]
= True()
m5(a,b,res,t) = [1] res + [1]
> [1] res + [0]
= res
monus(a,b) = [5]
> [0]
= m1(a,b,False(),False())
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(False()) = [0]
>= [0]
= 0()
bool2Nat(True()) = [0]
>= [0]
= S(0())
e1(a,b,res,t) = [1] t + [0]
>= [2]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [2]
>= [0]
= False()
e2(a,b,res,True()) = [2]
>= [2]
= e3(a,b,res,True())
e4(a,b,res,False()) = [1]
>= [0]
= False()
e4(a,b,res,True()) = [1]
>= [0]
= True()
e5(a,b,res,t) = [0]
>= [0]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [2] x + [2] y + [0]
>= [1] x + [2] y + [3]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [0]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [1] tmp + [1] x + [2] y + [3]
>= [1] mtmp + [1] res + [1] x + [2] y + [5]
= l2(x,y,res,tmp,mtmp,False())
l12(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [5]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [8]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,True(),t) = [2] y + [3]
>= [2] y + [0]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] mtmp + [1] res + [1] x + [2] y + [5]
>= [1] mtmp + [1] x + [2] y + [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] mtmp + [1] res + [1] x + [2] y + [5]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] x + [2] y + [0]
>= [1] x + [2] y + [0]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [3] res + [2] x + [1] x' + [0]
>= [2] res + [2] x + [1] x' + [0]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [2] res + [1] x + [2] y + [0]
>= [1] res + [1] x + [2] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [2] res + [1] x + [2] y + [0]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] res + [1] x + [2] y + [0]
>= [1] x + [2] y + [1]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [2] y + [1]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] x + [2] y + [1]
>= [1] x + [2] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [5] res + [0]
>= [3] res + [1]
= m2(a,x,res,False())
m2(a,b,res,False()) = [3] res + [1]
>= [1]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [3] res + [1]
>= [0]
= False()
m2(S(0()),b,res,True()) = [3] res + [1]
>= [0]
= False()
m3(0(),b,res,t) = [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [0]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [0]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [1]
>= [6]
= m5(S(x'),S(x),monus(x',x),t)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
bool2Nat(False()) -> 0()
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
equal0(a,b) -> e1(a,b,False(),False())
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e8(a,b,res,t) -> res
help1(0()) -> False()
help1(S(0())) -> False()
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [0]
= 0()
e5(a,b,res,t) = [2]
> [0]
= True()
equal0(a,b) = [5]
> [0]
= e1(a,b,False(),False())
help1(S(S(x))) = [6]
> [0]
= True()
l13(x,y,res,tmp,False(),t) = [1] y + [5]
> [1] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l8(x,y,res,False(),mtmp,t) = [2] res + [4] t + [1] x + [1] y + [6]
> [2] res + [1] x + [1] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [1] t + [4] tmp + [1] y + [1]
> [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [2] t + [4]
> [2] res + [1]
= m2(a,x,res,False())
m3(S(S(x)),b,res,t) = [1] b + [1] res + [1] t + [2]
> [0]
= True()
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(True()) = [5]
>= [5]
= S(0())
e1(a,b,res,t) = [3] res + [4] t + [0]
>= [3] res + [3]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [3] res + [3]
>= [0]
= False()
e2(a,b,res,True()) = [3] res + [3]
>= [2] res + [3]
= e3(a,b,res,True())
e3(a,b,res,t) = [2] res + [3]
>= [1] res + [3]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [1] res + [3]
>= [0]
= False()
e4(a,b,res,True()) = [1] res + [3]
>= [0]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [2] res + [1] t + [1]
>= [1] res + [0]
= res
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [0]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [1]
>= [0]
= False()
help1(S(0())) = [6]
>= [0]
= False()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [4] t + [4] tmp + [1] x + [1] y + [0]
>= [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [4]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [2] res + [1] x + [1] y + [4]
>= [1] y + [2]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] y + [2]
>= [1] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] y + [2]
>= [1] y + [2]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] t + [1] y + [2]
>= [1] y + [9]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,True(),t) = [1] y + [5]
>= [1] y + [5]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [4] t + [1] y + [0]
>= [1] y + [10]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1] y + [6]
>= [1] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1] y + [6]
>= [1] y + [5]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [4]
>= [1] res + [1] tmp + [1] x + [1] y + [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [4]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] res + [2] t + [1] tmp + [1] x + [1] y + [0]
>= [2] t + [1] x + [1] y + [0]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [2] res + [2] t + [1] x + [1] x' + [0]
>= [2] res + [1] x + [1] x' + [1]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [2] res + [1] x + [1] y + [1]
>= [2] res + [1] x + [1] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [2] res + [1] x + [1] y + [1]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [2] t + [4] x + [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [2] res + [4] t + [1] x + [1] y + [0]
>= [2] res + [4] t + [1] x + [1] y + [11]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [2] res' + [4] t + [1] y + [6]
>= [1] res + [0]
= res
m2(a,b,res,False()) = [2] res + [1]
>= [1] res + [1]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [2] res + [1]
>= [0]
= False()
m2(S(0()),b,res,True()) = [2] res + [1]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [2] res + [1]
>= [0]
= True()
m3(0(),b,res,t) = [1] b + [1] res + [1] t + [2]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] b + [1] res + [1] t + [2]
>= [0]
= False()
m4(S(x'),S(x),res,t) = [1] res + [2] t + [1]
>= [2] t + [10]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] res + [2] t + [6]
>= [1] res + [0]
= res
monus(a,b) = [4]
>= [4]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [2] mtmp + [4] res + [1] x + [2] y + [1]
= l2(x,y,res,tmp,mtmp,False())
Following rules are (at-least) weakly oriented:
<(x,0()) = [1]
>= [0]
= False()
<(0(),S(y)) = [1]
>= [0]
= True()
<(S(x),S(y)) = [1]
>= [1]
= <(x,y)
bool2Nat(False()) = [7]
>= [2]
= 0()
bool2Nat(True()) = [7]
>= [0]
= S(0())
e1(a,b,res,t) = [0]
>= [6]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [5]
>= [0]
= False()
e2(a,b,res,True()) = [5]
>= [1]
= e3(a,b,res,True())
e3(a,b,res,t) = [1]
>= [1]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [0]
>= [0]
= True()
e5(a,b,res,t) = [0]
>= [0]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [2] x + [2] y + [0]
>= [2] x + [2] y + [13]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [4]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l10(x,y,res,tmp,mtmp,t) = [2] res + [2] y + [1]
>= [2] y + [1]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] y + [0]
>= [2] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] y + [0]
>= [2] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [11]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [2] y + [7]
>= [2] y + [6]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [2] y + [7]
>= [2] y + [2]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [11]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [2] y + [7]
>= [2] y + [6]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [2] y + [7]
>= [2] y + [2]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [2]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [2] mtmp + [4] res + [1] x + [2] y + [1]
>= [2] mtmp + [1] x + [2] y + [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [2] mtmp + [4] res + [1] x + [2] y + [1]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] x + [2] y + [0]
>= [1] mtmp + [1] x + [2] y + [4]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [1] mtmp + [2] res + [2] x + [1] x' + [0]
>= [1] mtmp + [2] res + [2] x + [1] x' + [5]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] mtmp + [2] res + [1] x + [2] y + [5]
>= [1] mtmp + [2] res + [1] x + [2] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] mtmp + [2] res + [1] x + [2] y + [5]
>= [2]
= 0()
l6(x,y,res,tmp,mtmp,t) = [0]
>= [2]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] mtmp + [2] res + [1] x + [2] y + [0]
>= [1] mtmp + [2] res + [1] x + [2] y + [4]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] mtmp + [1] res + [2] res' + [2] y + [4]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] mtmp + [2] res + [1] x + [2] y + [4]
>= [2] res + [2] y + [1]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [4] t + [1]
>= [1] res + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [1] res + [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [1] res + [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [1] res + [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [1] res + [0]
>= [0]
= True()
m3(0(),b,res,t) = [2] t + [10]
>= [0]
= False()
m3(S(0()),b,res,t) = [2] t + [2]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [2] t + [2]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [1] t + [0]
>= [7]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] a + [1] res + [3]
>= [1] res + [0]
= res
monus(a,b) = [4]
>= [1]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: MI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [0]
= False()
e7(a,b,res,t) = [1] t + [1]
> [0]
= False()
l6(x,y,res,tmp,mtmp,t) = [2] mtmp + [4] x + [1]
> [0]
= 0()
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(False()) = [3]
>= [0]
= 0()
bool2Nat(True()) = [3]
>= [0]
= S(0())
e1(a,b,res,t) = [2] res + [0]
>= [2] res + [0]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [2] res + [0]
>= [0]
= False()
e2(a,b,res,True()) = [2] res + [0]
>= [1] res + [0]
= e3(a,b,res,True())
e3(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [1] res + [0]
>= [0]
= False()
e4(a,b,res,True()) = [1] res + [0]
>= [0]
= True()
e5(a,b,res,t) = [1] b + [4] t + [4]
>= [0]
= True()
e8(a,b,res,t) = [4] a + [1] b + [4] res + [2]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [4] x + [4] y + [0]
>= [4] x + [4] y + [0]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [0]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [2] res + [1] t + [4] x + [4] y + [0]
>= [1] mtmp + [2] res + [1] x + [4] y + [0]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] t + [1] x + [4] y + [0]
>= [1] mtmp + [4] y + [0]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] mtmp + [4] y + [0]
>= [4] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] mtmp + [4] y + [0]
>= [4] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [4] t + [4] y + [0]
>= [4] t + [4] y + [0]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [4] t + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] mtmp + [2] res + [1] x + [4] y + [0]
>= [1] mtmp + [1] x + [4] y + [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] mtmp + [2] res + [1] x + [4] y + [0]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] mtmp + [5] t + [1] x + [4] y + [0]
>= [1] mtmp + [4] t + [1] x + [4] y + [0]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [1] mtmp + [4] t + [4] x + [1] x' + [0]
>= [1] mtmp + [4] x + [1] x' + [0]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] mtmp + [1] x + [4] y + [0]
>= [1] mtmp + [1] x + [4] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] mtmp + [1] x + [4] y + [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] mtmp + [4] t + [1] x + [4] y + [0]
>= [1] mtmp + [4] t + [1] x + [4] y + [0]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] mtmp + [1] res + [4] t + [4] y + [0]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] mtmp + [4] t + [1] x + [4] y + [0]
>= [1] mtmp + [1] t + [1] x + [4] y + [0]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [2] res' + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [1] t + [0]
>= [1] res + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [1] res + [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [1] res + [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [1] res + [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [1] res + [0]
>= [0]
= True()
m3(0(),b,res,t) = [1] b + [4] t + [6]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] b + [4] t + [6]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [1] b + [4] t + [6]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [4] t + [0]
>= [2] t + [0]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [4] res + [2] t + [0]
>= [1] res + [0]
= res
monus(a,b) = [0]
>= [0]
= m1(a,b,False(),False())
* Step 7: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [1] x + [1] y + [0]
= l4(x,y,0(),tmp,mtmp,t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [1]
>= [1]
= False()
<(0(),S(y)) = [1]
>= [0]
= True()
<(S(x),S(y)) = [1]
>= [1]
= <(x,y)
bool2Nat(False()) = [2]
>= [0]
= 0()
bool2Nat(True()) = [2]
>= [2]
= S(0())
e1(a,b,res,t) = [3]
>= [4]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [4]
>= [1]
= False()
e2(a,b,res,True()) = [3]
>= [3]
= e3(a,b,res,True())
e3(a,b,res,t) = [3]
>= [2]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [2]
>= [1]
= False()
e4(a,b,res,True()) = [1]
>= [0]
= True()
e5(a,b,res,t) = [0]
>= [0]
= True()
e6(a,b,res,t) = [1]
>= [1]
= False()
e7(a,b,res,t) = [2]
>= [1]
= False()
e8(a,b,res,t) = [1] res + [1]
>= [1] res + [0]
= res
equal0(a,b) = [3]
>= [3]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [4]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [4]
>= [1]
= False()
help1(S(0())) = [4]
>= [1]
= False()
help1(S(S(x))) = [4]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [2] t + [1] x + [1] y + [1]
>= [1] res + [1] x + [1] y + [1]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] x + [1] y + [1]
>= [1] y + [1]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] y + [1]
>= [1] y + [1]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] y + [0]
>= [1] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [4] t + [1] y + [0]
>= [1] y + [9]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] y + [5]
>= [1] y + [5]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [1] y + [4]
>= [1] y + [4]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [1] y + [1]
>= [1] y + [9]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1] y + [5]
>= [1] y + [5]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1] y + [4]
>= [1] y + [4]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [3] mtmp + [1] res + [2]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] res + [1] x + [1] y + [1]
>= [1] x + [1] y + [1]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] res + [1] x + [1] y + [0]
>= [1] res + [0]
= res
l4(x',x,res,tmp,mtmp,t) = [1] x + [1] x' + [0]
>= [1] x + [1] x' + [6]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] x + [1] y + [6]
>= [1] x + [1] y + [2]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] x + [1] y + [5]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] t + [1] x + [1] y + [1]
>= [1] t + [1] x + [1] y + [3]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [1] t + [1] y + [0]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] t + [1] x + [1] y + [1]
>= [1] x + [1] y + [1]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [1] t + [3]
>= [3]
= m2(a,x,res,False())
m2(a,b,res,False()) = [3]
>= [3]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [1]
>= [1]
= False()
m2(S(0()),b,res,True()) = [1]
>= [1]
= False()
m2(S(S(x)),b,res,True()) = [1]
>= [0]
= True()
m3(0(),b,res,t) = [4] res + [1] t + [4]
>= [1]
= False()
m3(S(0()),b,res,t) = [4] res + [1] t + [12]
>= [1]
= False()
m3(S(S(x)),b,res,t) = [4] res + [1] t + [12]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [3]
>= [9]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] res + [4]
>= [1] res + [0]
= res
monus(a,b) = [5]
>= [4]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [3] res + [1] x + [1] x' + [0]
= l5(x',x,res,tmp,mtmp,False())
Following rules are (at-least) weakly oriented:
<(x,0()) = [3]
>= [0]
= False()
<(0(),S(y)) = [3]
>= [0]
= True()
<(S(x),S(y)) = [3]
>= [3]
= <(x,y)
bool2Nat(False()) = [4]
>= [0]
= 0()
bool2Nat(True()) = [4]
>= [0]
= S(0())
e1(a,b,res,t) = [5] res + [3]
>= [4] res + [6]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [4] res + [3]
>= [0]
= False()
e2(a,b,res,True()) = [4] res + [3]
>= [1] res + [3]
= e3(a,b,res,True())
e3(a,b,res,t) = [1] res + [3]
>= [3]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [0]
>= [0]
= True()
e5(a,b,res,t) = [0]
>= [0]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= res
equal0(a,b) = [3]
>= [3]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [2]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [1]
>= [0]
= False()
help1(S(0())) = [1]
>= [0]
= False()
help1(S(S(x))) = [1]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [1] t + [3] tmp + [1] x + [1] y + [2]
>= [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [2] res + [1] t + [2] tmp + [1] y + [4]
>= [1] res + [2] tmp + [1] y + [4]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] res + [2] tmp + [1] y + [1]
>= [1] y + [1]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] res + [2] tmp + [1] y + [1]
>= [1] res + [1] tmp + [1] y + [1]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] res + [1] tmp + [1] y + [1]
>= [1] res + [1] y + [1]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] res + [1] y + [0]
>= [1] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [1] res + [1] y + [0]
>= [1] y + [0]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [3] t + [1] y + [1]
>= [1] y + [1]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1] y + [0]
>= [1] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1] y + [0]
>= [1] y + [0]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
>= [2] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] res + [1] tmp + [1] x + [1] y + [2]
>= [1] tmp + [1] x + [1] y + [2]
= l4(x,y,0(),tmp,mtmp,t)
l5(x,y,res,tmp,mtmp,False()) = [3] res + [1] x + [1] y + [0]
>= [2] res + [1] x + [1] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [3] res + [1] x + [1] y + [0]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] res + [2] tmp + [1] x + [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [2] res + [4] t + [1] x + [1] y + [0]
>= [2] res + [1] t + [1] x + [1] y + [8]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [2] res' + [1] t + [1] y + [5]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [2] res + [1] t + [1] x + [1] y + [5]
>= [2] res + [1] t + [1] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [1] res + [1] tmp + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [5] res + [0]
>= [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [0]
>= [0]
= True()
m3(0(),b,res,t) = [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [0]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [0]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [1] t + [0]
>= [1] t + [2]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] a + [4] b + [1] res + [1] t + [1]
>= [1] res + [0]
= res
monus(a,b) = [1]
>= [0]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [3] mtmp + [4] t + [1] x + [2] y + [6]
= l8(x,y,res,equal0(x,y),mtmp,t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [4]
>= [0]
= False()
<(0(),S(y)) = [4]
>= [4]
= True()
<(S(x),S(y)) = [4]
>= [4]
= <(x,y)
bool2Nat(False()) = [2]
>= [1]
= 0()
bool2Nat(True()) = [10]
>= [4]
= S(0())
e1(a,b,res,t) = [3] res + [2] t + [0]
>= [2] res + [6]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [2] res + [2]
>= [0]
= False()
e2(a,b,res,True()) = [2] res + [6]
>= [5]
= e3(a,b,res,True())
e3(a,b,res,t) = [5]
>= [4]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [4]
>= [4]
= True()
e5(a,b,res,t) = [1] a + [1] b + [4]
>= [4]
= True()
e6(a,b,res,t) = [2] a + [1] res + [4] t + [5]
>= [0]
= False()
e7(a,b,res,t) = [2] t + [3]
>= [0]
= False()
e8(a,b,res,t) = [1] res + [1]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [2] y + [0]
>= [1] x + [2] y + [11]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [3]
>= [0]
= False()
help1(S(0())) = [6]
>= [0]
= False()
help1(S(S(x))) = [6]
>= [4]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [4] res + [1] t + [3] tmp + [1] x + [2] y + [7]
>= [4] mtmp + [2] res + [2] tmp + [1] x + [2] y + [7]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [3] mtmp + [1] t + [1] tmp + [1] x + [2] y + [4]
>= [2] mtmp + [1] tmp + [1] x + [2] y + [4]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] mtmp + [1] tmp + [1] x + [2] y + [0]
>= [1] mtmp + [1] tmp + [1] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] mtmp + [1] tmp + [1] x + [2] y + [4]
>= [2] mtmp + [1] tmp + [1] x + [2] y + [4]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] tmp + [1] x + [2] y + [4]
>= [1] x + [2] y + [8]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] x + [2] y + [4]
>= [2] y + [1]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [1] x + [2] y + [8]
>= [2] y + [4]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] tmp + [1] y + [0]
>= [1] y + [11]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1] y + [7]
>= [1] y + [2]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1] y + [11]
>= [1] y + [8]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [4] mtmp + [2] res + [2] tmp + [1] x + [2] y + [7]
>= [3] mtmp + [2] res + [2] tmp + [1] x + [2] y + [7]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [2] res + [2] tmp + [1] x + [2] y + [7]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [3] mtmp + [2] res + [2] tmp + [1] x + [2] y + [7]
>= [3] mtmp + [1] tmp + [1] x + [2] y + [7]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [3] mtmp + [1] tmp + [2] x + [1] x' + [7]
>= [3] mtmp + [2] x + [1] x' + [7]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [3] mtmp + [1] x + [2] y + [7]
>= [3] mtmp + [1] x + [2] y + [7]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [3] mtmp + [1] x + [2] y + [15]
>= [1]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] t + [1] tmp + [1] x + [4] y + [1]
>= [1]
= 0()
l8(res,y,res',True(),mtmp,t) = [3] mtmp + [1] res + [4] t + [2] y + [10]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [3] mtmp + [4] t + [1] x + [2] y + [6]
>= [3] mtmp + [1] t + [1] x + [2] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [1] res + [2] res' + [1] t + [2] tmp + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [1] res + [1] t + [0]
>= [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [8]
>= [0]
= False()
m2(S(0()),b,res,True()) = [8]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [8]
>= [4]
= True()
m3(0(),b,res,t) = [4] t + [5]
>= [0]
= False()
m3(S(0()),b,res,t) = [4] t + [8]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [4] t + [8]
>= [4]
= True()
m4(S(x'),S(x),res,t) = [1] t + [0]
>= [1] t + [8]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] b + [1] res + [1] t + [0]
>= [1] res + [0]
= res
monus(a,b) = [4]
>= [0]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 10: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [1]
= e2(a,b,res,<(a,b))
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(False()) = [0]
>= [0]
= 0()
bool2Nat(True()) = [0]
>= [0]
= S(0())
e2(a,b,res,False()) = [1]
>= [0]
= False()
e2(a,b,res,True()) = [1]
>= [1]
= e3(a,b,res,True())
e3(a,b,res,t) = [1]
>= [1]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [1]
>= [0]
= False()
e4(a,b,res,True()) = [1]
>= [0]
= True()
e5(a,b,res,t) = [0]
>= [0]
= True()
e6(a,b,res,t) = [0]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [1] res + [1]
>= [1] res + [0]
= res
equal0(a,b) = [2]
>= [2]
= e1(a,b,False(),False())
gcd(x,y) = [2] x + [2] y + [0]
>= [2] x + [2] y + [3]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [0]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] res + [2] x + [2] y + [3]
>= [4] res + [1] x + [2] y + [3]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [0]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] y + [0]
>= [2] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] y + [0]
>= [2] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [1]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [2] y + [0]
>= [2] y + [1]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [2] y + [0]
>= [2] y + [0]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [4] res + [1] x + [2] y + [3]
>= [1] x + [2] y + [3]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] res + [1] x + [2] y + [3]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] x + [2] y + [3]
>= [1] x + [2] y + [3]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [2] res + [2] x + [1] x' + [3]
>= [1] res + [2] x + [1] x' + [3]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] res + [1] x + [2] y + [3]
>= [1] res + [1] x + [2] y + [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] res + [1] x + [2] y + [3]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] mtmp + [2] res + [4] t + [1]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] res + [3] t + [1] x + [2] y + [3]
>= [1] res + [2] t + [1] x + [2] y + [3]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [1] res' + [2] t + [2] y + [1]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] res + [2] t + [1] x + [2] y + [1]
>= [2] y + [0]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [4] res + [2] t + [2] tmp + [2]
>= [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [1]
>= [4] res + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [4] res + [0]
>= [4] res + [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [4] res + [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [4] res + [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [4] res + [0]
>= [0]
= True()
m3(0(),b,res,t) = [2] b + [1] t + [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [2] b + [1] t + [0]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [2] b + [1] t + [0]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [4] res + [4] t + [0]
>= [6]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] a + [1] res + [5]
>= [1] res + [0]
= res
monus(a,b) = [1]
>= [1]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 11: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [1] t + [1] y + [2]
= l15(x,y,res,tmp,monus(x,y),t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(False()) = [1]
>= [1]
= 0()
bool2Nat(True()) = [1]
>= [0]
= S(0())
e1(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [1] res + [0]
>= [0]
= False()
e2(a,b,res,True()) = [1] res + [0]
>= [0]
= e3(a,b,res,True())
e3(a,b,res,t) = [0]
>= [0]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [0]
>= [0]
= True()
e5(a,b,res,t) = [1] a + [1] res + [1] t + [4]
>= [0]
= True()
e6(a,b,res,t) = [2] b + [0]
>= [0]
= False()
e7(a,b,res,t) = [1] b + [1] t + [5]
>= [0]
= False()
e8(a,b,res,t) = [4] b + [4] res + [1]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [5]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [5]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [1] t + [4] tmp + [1] x + [1] y + [4]
>= [1] res + [1] x + [1] y + [4]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] t + [4] tmp + [1] y + [3]
>= [2] tmp + [1] y + [3]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] tmp + [1] y + [3]
>= [1] y + [3]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] tmp + [1] y + [3]
>= [1] y + [3]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [5] t + [1] y + [3]
>= [2] t + [1] y + [4]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [2] t + [1] y + [4]
>= [1] y + [2]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [2] t + [1] y + [4]
>= [1] y + [1]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l15(x,y,res,tmp,False(),t) = [1] t + [1] y + [2]
>= [1] y + [2]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1] t + [1] y + [2]
>= [1] y + [1]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [1]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] res + [1] x + [1] y + [4]
>= [1] x + [1] y + [4]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] res + [1] x + [1] y + [4]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] t + [1] x + [1] y + [4]
>= [1] t + [1] x + [1] y + [3]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [1] t + [1] x + [1] x' + [3]
>= [1] x + [1] x' + [3]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] x + [1] y + [3]
>= [1] x + [1] y + [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] x + [1] y + [3]
>= [1]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] res + [1] x + [2]
>= [1]
= 0()
l7(x,y,res,tmp,mtmp,t) = [2] t + [1] x + [1] y + [3]
>= [1] t + [1] x + [1] y + [3]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [1] t + [1] y + [3]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] t + [1] x + [1] y + [3]
>= [1] t + [1] y + [3]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [4] mtmp + [2] res + [2] res' + [1] t + [2] y + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [1] t + [0]
>= [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [0]
>= [0]
= True()
m3(0(),b,res,t) = [1] b + [6]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] b + [4]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [1] b + [4]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [0]
>= [1]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] b + [1] res + [1]
>= [1] res + [0]
= res
monus(a,b) = [0]
>= [0]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 12: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [1] res + [2] tmp + [3] y + [0]
= l13(x,y,res,tmp,monus(x,y),t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
bool2Nat(False()) = [6]
>= [0]
= 0()
bool2Nat(True()) = [6]
>= [0]
= S(0())
e1(a,b,res,t) = [4] t + [0]
>= [0]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [0]
>= [0]
= False()
e2(a,b,res,True()) = [0]
>= [0]
= e3(a,b,res,True())
e3(a,b,res,t) = [4] t + [0]
>= [0]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [0]
>= [0]
= True()
e5(a,b,res,t) = [1] b + [4] res + [2] t + [5]
>= [0]
= True()
e6(a,b,res,t) = [4] a + [0]
>= [0]
= False()
e7(a,b,res,t) = [1] a + [1] b + [2] res + [4] t + [5]
>= [0]
= False()
e8(a,b,res,t) = [4] b + [1] res + [4] t + [4]
>= [1] res + [0]
= res
equal0(a,b) = [0]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [3] x + [3] y + [0]
>= [3] x + [3] y + [4]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [0]
>= [0]
= False()
help1(S(0())) = [0]
>= [0]
= False()
help1(S(S(x))) = [0]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [5] mtmp + [1] res + [2] t + [7] tmp + [3] x + [3] y + [4]
>= [1] res + [7] tmp + [3] x + [3] y + [4]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [3] res + [1] t + [2] tmp + [3] y + [3]
>= [3] res + [2] tmp + [3] y + [3]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [3] res + [2] tmp + [3] y + [3]
>= [3] res + [2] tmp + [3] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [3] res + [2] tmp + [3] y + [3]
>= [2] res + [2] tmp + [3] y + [2]
= l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) = [1] res + [2] tmp + [3] y + [0]
>= [3] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [1] res + [2] tmp + [3] y + [0]
>= [3] y + [0]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [3] res + [1] t + [2] tmp + [3] y + [0]
>= [3] y + [0]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [3] y + [0]
>= [3] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [3] y + [0]
>= [3] y + [0]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] res + [7] tmp + [3] x + [3] y + [4]
>= [1] res + [7] tmp + [3] x + [3] y + [4]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] res + [7] tmp + [3] x + [3] y + [4]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] res + [7] tmp + [3] x + [3] y + [4]
>= [4] tmp + [3] x + [3] y + [3]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [7] res + [4] tmp + [3] x + [3] x' + [3]
>= [5] res + [4] tmp + [3] x + [2] x' + [3]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [5] res + [4] tmp + [2] x + [3] y + [3]
>= [3] res + [2] x + [3] y + [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [5] res + [4] tmp + [2] x + [3] y + [3]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [4] mtmp + [2] res + [1] t + [2] x + [2] y + [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [3] res + [4] t + [2] x + [3] y + [3]
>= [3] res + [1] t + [2] x + [3] y + [3]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [2] res + [3] res' + [1] t + [3] y + [3]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [3] res + [1] t + [2] x + [3] y + [3]
>= [3] res + [1] t + [3] y + [3]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [4] res + [4] res' + [4] y + [2]
>= [1] res + [0]
= res
m1(a,x,res,t) = [0]
>= [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0]
>= [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [0]
>= [0]
= True()
m3(0(),b,res,t) = [1] t + [2]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] t + [2]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [1] t + [1] x + [2]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [0]
>= [7]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] res + [7]
>= [1] res + [0]
= res
monus(a,b) = [0]
>= [0]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 13: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [2] x' + [0]
= m5(S(x'),S(x),monus(x',x),t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [3]
>= [0]
= False()
<(0(),S(y)) = [3]
>= [3]
= True()
<(S(x),S(y)) = [3]
>= [3]
= <(x,y)
bool2Nat(False()) = [1]
>= [0]
= 0()
bool2Nat(True()) = [1]
>= [1]
= S(0())
e1(a,b,res,t) = [5] res + [2] t + [3]
>= [4] res + [3]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [4] res + [0]
>= [0]
= False()
e2(a,b,res,True()) = [4] res + [3]
>= [1] res + [3]
= e3(a,b,res,True())
e3(a,b,res,t) = [1] res + [3]
>= [3]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [3]
>= [3]
= True()
e5(a,b,res,t) = [1] b + [3]
>= [3]
= True()
e6(a,b,res,t) = [2] b + [1] res + [4]
>= [0]
= False()
e7(a,b,res,t) = [1] a + [4] t + [1]
>= [0]
= False()
e8(a,b,res,t) = [1] a + [1] b + [4] res + [1] t + [0]
>= [1] res + [0]
= res
equal0(a,b) = [3]
>= [3]
= e1(a,b,False(),False())
gcd(x,y) = [4] x + [4] y + [0]
>= [4] x + [4] y + [7]
= l1(x,y,0(),False(),False(),False())
help1(0()) = [4]
>= [0]
= False()
help1(S(0())) = [8]
>= [0]
= False()
help1(S(S(x))) = [4] x + [12]
>= [3]
= True()
l1(x,y,res,tmp,mtmp,t) = [6] mtmp + [2] res + [4] tmp + [4] x + [4] y + [7]
>= [4] mtmp + [2] res + [4] tmp + [4] x + [4] y + [7]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] mtmp + [2] t + [5] tmp + [4] x + [4] y + [4]
>= [1] mtmp + [5] tmp + [4] x + [4] y + [4]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] mtmp + [5] tmp + [4] x + [4] y + [1]
>= [5] tmp + [2] x + [4] y + [1]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] mtmp + [5] tmp + [4] x + [4] y + [4]
>= [1] mtmp + [3] x + [4] y + [4]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] mtmp + [3] x + [4] y + [4]
>= [2] x + [4] y + [4]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [4] y + [4]
>= [4] y + [0]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [4] y + [7]
>= [4] y + [4]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [1] t + [5] tmp + [2] x + [4] y + [1]
>= [2] x + [4] y + [1]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [4] y + [1]
>= [4] y + [0]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [4] y + [4]
>= [4] y + [4]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [4] mtmp + [2] res + [4] tmp + [4] x + [4] y + [7]
>= [3] mtmp + [1] tmp + [4] x + [4] y + [7]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [2] res + [4] tmp + [4] x + [4] y + [7]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [3] mtmp + [1] t + [1] tmp + [4] x + [4] y + [7]
>= [3] mtmp + [4] x + [4] y + [7]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [3] mtmp + [5] res + [4] x + [4] x' + [7]
>= [2] mtmp + [1] res + [4] x + [4] x' + [7]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [2] mtmp + [1] res + [4] x + [4] y + [7]
>= [2] mtmp + [1] res + [4] x + [4] y + [7]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [2] mtmp + [1] res + [4] x + [4] y + [7]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [1] t + [1] tmp + [5]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] res + [2] t + [4] x + [4] y + [7]
>= [2] mtmp + [2] t + [4] x + [4] y + [7]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [2] mtmp + [4] res + [2] t + [4] y + [7]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [2] mtmp + [2] t + [4] x + [4] y + [4]
>= [1] mtmp + [2] t + [4] x + [4] y + [4]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] res + [1] res' + [1] tmp + [4] y + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [2] a + [2] res + [1] t + [0]
>= [2] a + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [2] a + [0]
>= [2] a + [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [2]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [2] x + [4]
>= [3]
= True()
m3(0(),b,res,t) = [2] b + [1] t + [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [2] b + [1] t + [6]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [2] b + [1] t + [6] x + [12]
>= [3]
= True()
m5(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= res
monus(a,b) = [2] a + [0]
>= [2] a + [0]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 14: MI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{ [7 5] x + [7 6] y + [1]
[7 5] [7 6] [4]
= l1(x,y,0(),False(),False(),False())
Following rules are (at-least) weakly oriented:
<(x,0()) = [0 0] x + [1]
[3 3] [0]
>= [1]
[0]
= False()
<(0(),S(y)) = [1]
[3]
>= [0]
[3]
= True()
<(S(x),S(y)) = [0 0] x + [1]
[3 3] [0]
>= [0 0] x + [1]
[3 3] [0]
= <(x,y)
bool2Nat(False()) = [1]
[6]
>= [0]
[1]
= 0()
bool2Nat(True()) = [3]
[7]
>= [1]
[0]
= S(0())
e1(a,b,res,t) = [3 3] a + [0 2] res + [0 0] t + [1]
[7 5] [0 4] [0 2] [1]
>= [3 3] a + [0 2] res + [1]
[7 4] [0 4] [1]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [0 0] a + [0 2] res + [1]
[4 1] [0 4] [1]
>= [1]
[0]
= False()
e2(a,b,res,True()) = [0 0] a + [0 2] res + [3]
[4 1] [0 4] [4]
>= [0 0] a + [0 2] res + [1]
[0 1] [0 2] [4]
= e3(a,b,res,True())
e3(a,b,res,t) = [0 0] a + [0 2] res + [1]
[0 1] [0 2] [4]
>= [0 0] a + [0 0] res + [1]
[0 1] [0 2] [3]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0 0] a + [0 0] res + [1]
[0 1] [0 2] [3]
>= [1]
[0]
= False()
e4(a,b,res,True()) = [0 0] a + [0 0] res + [0]
[0 1] [0 2] [3]
>= [0]
[3]
= True()
e5(a,b,res,t) = [1 4] t + [0]
[0 0] [4]
>= [0]
[3]
= True()
e6(a,b,res,t) = [1 1] b + [1 2] res + [0 0] t + [4]
[1 2] [1 1] [4 1] [0]
>= [1]
[0]
= False()
e7(a,b,res,t) = [1 0] a + [4]
[1 1] [1]
>= [1]
[0]
= False()
e8(a,b,res,t) = [1 1] a + [0 0] b + [4 1] res + [1 1] t + [1]
[1 1] [1 1] [0 2] [1 4] [0]
>= [1 0] res + [0]
[0 1] [0]
= res
equal0(a,b) = [3 3] a + [1]
[7 5] [1]
>= [3 3] a + [1]
[7 5] [1]
= e1(a,b,False(),False())
help1(0()) = [1]
[6]
>= [1]
[0]
= False()
help1(S(0())) = [1]
[7]
>= [1]
[0]
= False()
help1(S(S(x))) = [0 0] x + [1]
[1 1] [6]
>= [0]
[3]
= True()
l1(x,y,res,tmp,mtmp,t) = [1 0] res + [0 1] t + [0 4] tmp + [7 5] x + [7 6] y + [1]
[2 1] [0 4] [0 0] [7 5] [7 6] [3]
>= [1 0] res + [7 5] x + [7 6] y + [1]
[1 1] [7 5] [7 6] [3]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [2 0] res + [0 0] tmp + [4 2] x + [7 6] y + [1]
[0 0] [0 6] [4 2] [7 6] [3]
>= [2 0] res + [0 0] tmp + [4 2] x + [7 6] y + [1]
[0 0] [0 4] [4 2] [7 6] [3]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2 0] res + [0 0] tmp + [4 2] x + [7 6] y + [1]
[0 0] [0 4] [4 2] [7 6] [3]
>= [1 0] res + [4 1] x + [7 6] y + [1]
[0 0] [4 2] [7 6] [3]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2 0] res + [0 0] tmp + [4 2] x + [7 6] y + [0]
[0 0] [0 4] [4 2] [7 6] [3]
>= [4 0] x + [7 6] y + [0]
[4 2] [7 6] [3]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [4 0] x + [7 6] y + [0]
[4 2] [7 6] [3]
>= [3 0] x + [7 6] y + [0]
[4 2] [7 6] [3]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [0 0] x + [7 6] y + [7]
[0 2] [7 6] [10]
>= [0 0] x + [7 6] y + [7]
[0 1] [7 6] [10]
= l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) = [0 0] x + [7 6] y + [9]
[0 2] [7 6] [15]
>= [0 0] x + [7 6] y + [9]
[0 1] [7 6] [11]
= l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) = [1 0] res + [0 0] t + [4 1] x + [7 6] y + [1]
[0 0] [0 1] [4 2] [7 6] [3]
>= [1 0] res + [0 0] t + [4 1] x + [7 5] y + [1]
[0 0] [0 1] [4 1] [7 6] [3]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1 0] res + [0 0] t + [0 1] x + [7 5] y + [8]
[0 0] [0 1] [0 1] [7 6] [10]
>= [0 0] x + [7 5] y + [8]
[0 1] [7 6] [10]
= l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) = [1 0] res + [0 0] t + [0 1] x + [7 5] y + [13]
[0 0] [0 1] [0 1] [7 6] [15]
>= [0 0] x + [7 5] y + [9]
[0 1] [7 6] [11]
= l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) = [1 0] res + [0 0] x + [0]
[0 1] [0 1] [0]
>= [1 0] res + [0]
[0 1] [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1 0] res + [7 5] x + [7 6] y + [1]
[1 1] [7 5] [7 6] [3]
>= [7 5] x + [7 6] y + [1]
[7 5] [7 6] [3]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1 0] res + [7 5] x + [7 6] y + [13]
[1 1] [7 5] [7 6] [0]
>= [1 0] res + [0]
[0 1] [0]
= res
l3(x,y,res,tmp,mtmp,t) = [0 0] t + [7 5] x + [7 6] y + [1]
[0 4] [7 5] [7 6] [3]
>= [7 5] x + [7 6] y + [1]
[7 5] [7 6] [3]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [4 0] res + [7 6] x + [7 5] x' + [1]
[4 0] [7 6] [7 5] [3]
>= [3 0] res + [7 6] x + [7 5] x' + [1]
[1 0] [7 6] [7 5] [3]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [3 0] res + [7 5] x + [7 6] y + [1]
[1 0] [7 5] [7 6] [3]
>= [3 0] res + [7 5] x + [7 6] y + [1]
[0 0] [7 5] [7 6] [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [3 0] res + [7 5] x + [7 6] y + [1]
[1 0] [7 5] [7 6] [3]
>= [0]
[1]
= 0()
l6(x,y,res,tmp,mtmp,t) = [0 2] mtmp + [0 2] res + [0 1] t + [1 0] y + [1]
[2 1] [2 2] [2 1] [0 1] [2]
>= [0]
[1]
= 0()
l7(x,y,res,tmp,mtmp,t) = [3 0] res + [7 5] x + [7 6] y + [1]
[0 0] [7 5] [7 6] [3]
>= [3 0] res + [7 5] x + [7 6] y + [1]
[0 0] [7 5] [7 6] [3]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [4 2] res + [3 0] res' + [7 6] y + [0]
[4 2] [0 0] [7 6] [2]
>= [1 0] res + [0]
[0 1] [0]
= res
l8(x,y,res,False(),mtmp,t) = [3 0] res + [4 2] x + [7 6] y + [1]
[0 0] [4 2] [7 6] [3]
>= [2 0] res + [4 2] x + [7 6] y + [1]
[0 0] [4 2] [7 6] [3]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [0 1] mtmp + [2 4] res + [0 0] t + [1 1] tmp + [0 0] y + [1]
[2 1] [2 1] [2 0] [1 0] [0 4] [4]
>= [1 0] res + [0]
[0 1] [0]
= res
m1(a,x,res,t) = [0 0] a + [0 0] res + [0 0] t + [0]
[1 0] [0 4] [0 2] [0]
>= [0 0] a + [0 0] res + [0]
[1 0] [0 2] [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0 0] a + [0 0] res + [0]
[1 0] [0 2] [0]
>= [0 0] a + [0 0] res + [0]
[1 0] [0 1] [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0 0] res + [9]
[0 2] [3]
>= [1]
[0]
= False()
m2(S(0()),b,res,True()) = [0 0] res + [9]
[0 2] [4]
>= [1]
[0]
= False()
m2(S(S(x)),b,res,True()) = [0 0] res + [0 0] x + [9]
[0 2] [1 1] [3]
>= [0]
[3]
= True()
m3(0(),b,res,t) = [2 0] res + [0 0] t + [7]
[2 1] [0 1] [5]
>= [1]
[0]
= False()
m3(S(0()),b,res,t) = [2 0] res + [0 0] t + [5]
[2 1] [0 1] [4]
>= [1]
[0]
= False()
m3(S(S(x)),b,res,t) = [2 0] res + [0 0] t + [4 4] x + [1]
[2 1] [0 1] [0 0] [4]
>= [0]
[3]
= True()
m4(S(x'),S(x),res,t) = [0 0] res + [0 0] t + [0 0] x' + [0]
[0 1] [0 4] [1 1] [0]
>= [0 0] x' + [0]
[1 0] [0]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [2 0] res + [0]
[0 1] [0]
>= [1 0] res + [0]
[0 1] [0]
= res
monus(a,b) = [0 0] a + [0]
[1 0] [0]
>= [0 0] a + [0]
[1 0] [0]
= m1(a,b,False(),False())
* Step 15: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bool2Nat(False()) -> 0()
bool2Nat(True()) -> S(0())
e1(a,b,res,t) -> e2(a,b,res,<(a,b))
e2(a,b,res,False()) -> False()
e2(a,b,res,True()) -> e3(a,b,res,True())
e3(a,b,res,t) -> e4(a,b,res,<(b,a))
e4(a,b,res,False()) -> False()
e4(a,b,res,True()) -> True()
e5(a,b,res,t) -> True()
e6(a,b,res,t) -> False()
e7(a,b,res,t) -> False()
e8(a,b,res,t) -> res
equal0(a,b) -> e1(a,b,False(),False())
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
help1(0()) -> False()
help1(S(0())) -> False()
help1(S(S(x))) -> True()
l1(x,y,res,tmp,mtmp,t) -> l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) -> l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) -> l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) -> l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) -> l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) -> l16(x,y,gcd(0(),y),tmp,False(),t)
l13(x,y,res,tmp,True(),t) -> l16(x,y,gcd(S(0()),y),tmp,True(),t)
l14(x,y,res,tmp,mtmp,t) -> l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) -> l16(x,y,gcd(y,0()),tmp,False(),t)
l15(x,y,res,tmp,True(),t) -> l16(x,y,gcd(y,S(0())),tmp,True(),t)
l16(x,y,res,tmp,mtmp,t) -> res
l2(x,y,res,tmp,mtmp,False()) -> l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) -> res
l3(x,y,res,tmp,mtmp,t) -> l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) -> l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) -> l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) -> 0()
l6(x,y,res,tmp,mtmp,t) -> 0()
l7(x,y,res,tmp,mtmp,t) -> l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) -> res
l8(x,y,res,False(),mtmp,t) -> l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) -> res
m1(a,x,res,t) -> m2(a,x,res,False())
m2(a,b,res,False()) -> m4(a,b,res,False())
m2(0(),b,res,True()) -> False()
m2(S(0()),b,res,True()) -> False()
m2(S(S(x)),b,res,True()) -> True()
m3(0(),b,res,t) -> False()
m3(S(0()),b,res,t) -> False()
m3(S(S(x)),b,res,t) -> True()
m4(S(x'),S(x),res,t) -> m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) -> res
monus(a,b) -> m1(a,b,False(),False())
- Signature:
{