*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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.
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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.
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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.
*** 1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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]
> [0]
= False()
l3(x,y,res,tmp,mtmp,t) = [4] mtmp + [2] x + [2] y + [6]
> [1] x + [2] y + [5]
= l4(x,y,0(),tmp,mtmp,t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [1]
>= [0]
= False()
<(0(),S(y)) = [1]
>= [1]
= True()
<(S(x),S(y)) = [1]
>= [1]
= <(x,y)
bool2Nat(False()) = [2]
>= [1]
= 0()
bool2Nat(True()) = [4]
>= [4]
= S(0())
e1(a,b,res,t) = [1] res + [0]
>= [1] res + [6]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [1] res + [5]
>= [0]
= False()
e2(a,b,res,True()) = [1] res + [6]
>= [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()) = [1]
>= [1]
= True()
e5(a,b,res,t) = [1]
>= [1]
= True()
e8(a,b,res,t) = [1] res + [0]
>= [1] res + [0]
= res
equal0(a,b) = [5]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [2] x + [2] y + [0]
>= [2] x + [2] y + [7]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [4]
>= [0]
= False()
help1(S(0())) = [7]
>= [0]
= False()
help1(S(S(x))) = [7]
>= [1]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [2] x + [2] y + [6]
>= [4] mtmp + [1] res + [2] x + [2] y + [6]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] t + [2] tmp + [1] x + [2] y + [2]
>= [2] tmp + [1] x + [2] y + [1]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] tmp + [1] x + [2] y + [0]
>= [2] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] tmp + [1] x + [2] y + [1]
>= [2] tmp + [1] x + [2] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [2] tmp + [1] x + [2] y + [0]
>= [1] x + [2] y + [12]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] x + [2] y + [7]
>= [2] y + [2]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [1] x + [2] y + [8]
>= [2] y + [8]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [5] t + [2] y + [0]
>= [2] y + [12]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [2] y + [7]
>= [2] y + [2]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [2] y + [8]
>= [2] 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 + [1] res + [2] x + [2] y + [6]
>= [4] mtmp + [2] x + [2] y + [6]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [1] res + [2] x + [2] y + [11]
>= [1] res + [0]
= res
l4(x',x,res,tmp,mtmp,t) = [5] 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 + [1]
>= [1]
= 0()
l6(x,y,res,tmp,mtmp,t) = [0]
>= [1]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] res + [4] t + [1] x + [2] y + [0]
>= [1] res + [4] t + [1] x + [2] y + [12]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [1] res' + [4] t + [2] y + [8]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] res + [4] t + [1] x + [2] y + [7]
>= [1] t + [1] x + [2] y + [2]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [1] res + [1] t + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [5]
>= [4]
= m2(a,x,res,False())
m2(a,b,res,False()) = [4]
>= [4]
= 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]
>= [1]
= True()
m3(0(),b,res,t) = [1] b + [4] res + [1]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] b + [4] res + [1]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [1] b + [4] res + [1]
>= [1]
= True()
m4(S(x'),S(x),res,t) = [4]
>= [14]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [2] b + [1] res + [1]
>= [1] res + [0]
= res
monus(a,b) = [5]
>= [5]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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())
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 DP Rules:
Weak TRS Rules:
<(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()
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:
{ [4] res + [0]
= e2(a,b,res,<(a,b))
l6(x,y,res,tmp,mtmp,t) = [2] res + [1] t + [5]
> [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()) = [1]
>= [0]
= 0()
bool2Nat(True()) = [1]
>= [0]
= S(0())
e2(a,b,res,False()) = [4] res + [0]
>= [0]
= False()
e2(a,b,res,True()) = [4] res + [0]
>= [4] res + [0]
= e3(a,b,res,True())
e3(a,b,res,t) = [4] res + [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) = [4] a + [1] b + [4]
>= [0]
= True()
e6(a,b,res,t) = [4] a + [4] b + [4] t + [0]
>= [0]
= False()
e7(a,b,res,t) = [1] a + [1] b + [2] res + [1] t + [3]
>= [0]
= False()
e8(a,b,res,t) = [1] a + [2] res + [1]
>= [1] res + [0]
= res
equal0(a,b) = [2] a + [6]
>= [2] a + [3]
= e1(a,b,False(),False())
gcd(x,y) = [3] x + [3] y + [2]
>= [3] x + [3] y + [2]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [6]
>= [0]
= False()
help1(S(0())) = [6]
>= [0]
= False()
help1(S(S(x))) = [6]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [1] res + [1] t + [4] tmp + [3] x + [3] y + [2]
>= [3] mtmp + [1] res + [2] tmp + [3] x + [3] y + [2]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [3] tmp + [1] x + [3] y + [2]
>= [1] mtmp + [1] tmp + [3] y + [2]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] mtmp + [1] tmp + [3] y + [2]
>= [1] mtmp + [1] tmp + [3] y + [1]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] mtmp + [1] tmp + [3] y + [2]
>= [1] mtmp + [1] tmp + [3] y + [2]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] mtmp + [4] t + [1] tmp + [3] y + [2]
>= [1] t + [3] y + [5]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] t + [3] y + [2]
>= [3] y + [2]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [1] t + [3] y + [2]
>= [3] y + [2]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [1] mtmp + [3] t + [1] tmp + [3] y + [1]
>= [2] t + [1] tmp + [3] y + [5]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [2] t + [1] tmp + [3] y + [2]
>= [3] y + [2]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [2] t + [1] tmp + [3] y + [2]
>= [3] y + [2]
= 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()) = [3] mtmp + [1] res + [2] tmp + [3] x + [3] y + [2]
>= [3] mtmp + [2] tmp + [3] x + [3] y + [1]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [3] mtmp + [1] res + [2] tmp + [3] x + [3] y + [2]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [3] mtmp + [1] t + [2] tmp + [3] x + [3] y + [1]
>= [3] mtmp + [3] x + [3] y + [1]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [3] mtmp + [1] res + [3] x + [3] x' + [1]
>= [2] mtmp + [1] res + [3] x + [3] x' + [7]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [2] mtmp + [1] res + [3] x + [3] y + [7]
>= [1] mtmp + [1] res + [3] x + [3] y + [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [2] mtmp + [1] res + [3] x + [3] y + [7]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [3] x + [3] y + [3]
>= [1] mtmp + [1] res + [3] x + [3] y + [12]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] mtmp + [1] res + [1] res' + [3] y + [6]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [1] mtmp + [1] res + [1] x + [3] y + [6]
>= [1] mtmp + [1] res + [1] x + [3] y + [2]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [4] res + [4] res' + [1] t + [1] y + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [4] res + [3]
>= [1] res + [2]
= m2(a,x,res,False())
m2(a,b,res,False()) = [1] res + [2]
>= [2]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [1] res + [2]
>= [0]
= False()
m2(S(0()),b,res,True()) = [1] res + [2]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [1] res + [2]
>= [0]
= True()
m3(0(),b,res,t) = [1] res + [1] t + [4]
>= [0]
= False()
m3(S(0()),b,res,t) = [1] res + [1] t + [4]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [1] res + [1] t + [4]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [3] t + [2]
>= [5]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [2] a + [1] b + [1] res + [2]
>= [1] res + [0]
= res
monus(a,b) = [3]
>= [3]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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)
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] mtmp + [2] res + [3] x + [1] x' + [1]
= l5(x',x,res,tmp,mtmp,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()) = [2]
>= [0]
= 0()
bool2Nat(True()) = [2]
>= [1]
= S(0())
e1(a,b,res,t) = [1]
>= [1]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [1]
>= [0]
= False()
e2(a,b,res,True()) = [1]
>= [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) = [4]
>= [0]
= True()
e6(a,b,res,t) = [1]
>= [0]
= False()
e7(a,b,res,t) = [0]
>= [0]
= False()
e8(a,b,res,t) = [2] res + [0]
>= [1] res + [0]
= res
equal0(a,b) = [1]
>= [1]
= e1(a,b,False(),False())
gcd(x,y) = [2] x + [3] y + [0]
>= [1] x + [3] y + [5]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [0]
>= [0]
= False()
help1(S(0())) = [1]
>= [0]
= False()
help1(S(S(x))) = [1]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] res + [1] tmp + [1] x + [3] y + [5]
>= [1] mtmp + [1] res + [1] tmp + [1] x + [3] y + [5]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] x + [3] y + [6]
>= [3] y + [6]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [3] y + [6]
>= [3] y + [6]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [3] y + [6]
>= [3] y + [4]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [3] y + [4]
>= [3] y + [9]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [3] y + [2]
>= [3] y + [0]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [3] y + [2]
>= [3] y + [2]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [1] t + [3] y + [6]
>= [3] y + [11]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [3] y + [4]
>= [2] y + [0]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [3] y + [4]
>= [2] y + [3]
= l16(x
,y
,gcd(y,S(0()))
,tmp
,True()
,t)
l16(x,y,res,tmp,mtmp,t) = [2] mtmp + [1] res + [0]
>= [1] res + [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1] mtmp + [1] res + [1] tmp + [1] x + [3] y + [5]
>= [1] mtmp + [1] x + [3] y + [5]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] mtmp + [1] res + [1] tmp + [1] x + [3] y + [5]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] t + [1] x + [3] y + [5]
>= [1] mtmp + [1] t + [1] x + [3] y + [5]
= l4(x,y,0(),tmp,mtmp,t)
l5(x,y,res,tmp,mtmp,False()) = [1] mtmp + [2] res + [1] x + [3] y + [1]
>= [1] x + [3] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] mtmp + [2] res + [1] x + [3] y + [1]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] mtmp + [1] t + [1] y + [0]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [7] t + [1] x + [3] y + [0]
>= [4] t + [1] x + [3] y + [8]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [4] t + [3] y + [7]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [4] t + [1] x + [3] y + [7]
>= [1] x + [3] y + [6]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [4] mtmp + [1] res + [4] res' + [1] t + [1]
>= [1] res + [0]
= res
m1(a,x,res,t) = [6] res + [4] t + [7]
>= [5] res + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [5] res + [0]
>= [4] res + [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [5] res + [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [5] res + [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [5] res + [0]
>= [0]
= True()
m3(0(),b,res,t) = [2] t + [3]
>= [0]
= False()
m3(S(0()),b,res,t) = [2] t + [3]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [2] t + [3]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [4] res + [0]
>= [13]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1] res + [6]
>= [1] res + [0]
= res
monus(a,b) = [7]
>= [7]
= m1(a,b,False(),False())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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()
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] tmp + [1] y + [0]
= l15(x,y,res,tmp,monus(x,y),t)
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()) = [0]
>= [0]
= 0()
bool2Nat(True()) = [0]
>= [0]
= S(0())
e1(a,b,res,t) = [7]
>= [7]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [4]
>= [0]
= False()
e2(a,b,res,True()) = [4]
>= [4]
= e3(a,b,res,True())
e3(a,b,res,t) = [4]
>= [4]
= 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 + [0]
>= [1] res + [0]
= res
equal0(a,b) = [7]
>= [7]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [4] y + [0]
>= [1] x + [4] y + [1]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [2]
>= [0]
= False()
help1(S(0())) = [2]
>= [0]
= False()
help1(S(S(x))) = [2]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [1] res + [1] x + [4] y + [1]
>= [1] res + [1] x + [4] y + [1]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [2] tmp + [4] y + [5]
>= [2] tmp + [4] y + [5]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] tmp + [4] y + [2]
>= [2] tmp + [1] y + [1]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] tmp + [4] y + [2]
>= [1] tmp + [4] y + [2]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] tmp + [4] y + [2]
>= [4] y + [3]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [4] y + [3]
>= [4] y + [0]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [4] y + [3]
>= [4] y + [0]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l15(x,y,res,tmp,False(),t) = [1] tmp + [1] y + [0]
>= [1] y + [0]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [1] tmp + [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()) = [1] res + [1] x + [4] y + [1]
>= [1] x + [4] y + [1]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] res + [1] x + [4] y + [1]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] x + [4] y + [1]
>= [1] x + [4] y + [0]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [4] x + [1] x' + [0]
>= [4] x + [1] x' + [0]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] x + [4] y + [0]
>= [1] x + [4] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] x + [4] y + [0]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] tmp + [2] x + [1] y + [4]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [6] t + [1] x + [4] y + [0]
>= [4] t + [1] x + [4] y + [13]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [4] t + [4] y + [6]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [4] t + [1] x + [4] y + [6]
>= [4] y + [5]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [4] res + [2] t + [2] tmp + [0]
>= [1] res + [0]
= res
m1(a,x,res,t) = [3] res + [0]
>= [2] res + [0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [2] res + [0]
>= [2] res + [0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [2] res + [0]
>= [0]
= False()
m2(S(0()),b,res,True()) = [2] res + [0]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [2] res + [0]
>= [0]
= True()
m3(0(),b,res,t) = [2] b + [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [2] b + [0]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [2] b + [0]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [2] res + [1] t + [0]
>= [1]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [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.
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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)
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 DP Rules:
Weak TRS Rules:
<(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()
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] res + [1] x + [4] y + [0]
= l13(x,y,res,tmp,monus(x,y),t)
Following rules are (at-least) weakly oriented:
<(x,0()) = [2]
>= [0]
= False()
<(0(),S(y)) = [2]
>= [2]
= True()
<(S(x),S(y)) = [2]
>= [2]
= <(x,y)
bool2Nat(False()) = [0]
>= [0]
= 0()
bool2Nat(True()) = [0]
>= [0]
= S(0())
e1(a,b,res,t) = [4] res + [2]
>= [2]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [0]
>= [0]
= False()
e2(a,b,res,True()) = [2]
>= [2]
= e3(a,b,res,True())
e3(a,b,res,t) = [2]
>= [2]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0]
>= [0]
= False()
e4(a,b,res,True()) = [2]
>= [2]
= True()
e5(a,b,res,t) = [1] t + [3]
>= [2]
= True()
e6(a,b,res,t) = [1] a + [2] b + [1] res + [1] t + [0]
>= [0]
= False()
e7(a,b,res,t) = [1] a + [1] b + [4] res + [2] t + [0]
>= [0]
= False()
e8(a,b,res,t) = [1] a + [1] b + [1] res + [4] t + [0]
>= [1] res + [0]
= res
equal0(a,b) = [4]
>= [2]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [4] y + [0]
>= [1] x + [4] y + [5]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [3]
>= [0]
= False()
help1(S(0())) = [3]
>= [0]
= False()
help1(S(S(x))) = [3]
>= [2]
= True()
l1(x,y,res,tmp,mtmp,t) = [4] mtmp + [4] res + [1] t + [2] tmp + [1] x + [4] y + [5]
>= [4] mtmp + [4] res + [1] tmp + [1] x + [4] y + [4]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [3] res + [6] tmp + [1] x + [4] y + [7]
>= [2] res + [4] tmp + [1] x + [4] y + [7]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [2] res + [4] tmp + [1] x + [4] y + [5]
>= [2] res + [3] tmp + [1] x + [2] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [2] res + [4] tmp + [1] x + [4] y + [7]
>= [2] res + [1] x + [4] y + [7]
= l12(x,y,res,tmp,mtmp,True())
l13(x,y,res,tmp,False(),t) = [2] res + [1] x + [4] y + [0]
>= [4] y + [0]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [2] res + [1] x + [4] y + [2]
>= [4] y + [0]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [2] res + [5] t + [3] tmp + [1] x + [2] y + [0]
>= [2] t + [2] tmp + [1] x + [1] y + [0]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [2] t + [2] tmp + [1] x + [1] y + [0]
>= [1] y + [0]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [2] t + [2] tmp + [1] x + [1] y + [2]
>= [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 + [4] res + [1] tmp + [1] x + [4] y + [4]
>= [1] x + [4] y + [2]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [4] mtmp + [4] res + [1] tmp + [1] x + [4] y + [6]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [2] t + [1] x + [4] y + [2]
>= [1] x + [4] y + [1]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [7] res + [4] x + [1] x' + [1]
>= [4] res + [4] x + [1] x' + [1]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [4] res + [1] x + [4] y + [1]
>= [4] res + [1] x + [4] y + [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [4] res + [1] x + [4] y + [1]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [1] res + [1] tmp + [1] x + [2] y + [1]
>= [0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [4] res + [1] t + [1] x + [4] y + [0]
>= [3] res + [1] x + [4] y + [11]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [1] res + [3] res' + [4] y + [9]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [3] res + [1] x + [4] y + [7]
>= [3] res + [1] x + [4] y + [7]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1] mtmp + [4] res + [1] res' + [2] y + [0]
>= [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()) = [8]
>= [0]
= False()
m2(S(0()),b,res,True()) = [8]
>= [0]
= False()
m2(S(S(x)),b,res,True()) = [8]
>= [2]
= True()
m3(0(),b,res,t) = [4] b + [4] res + [1] t + [3]
>= [0]
= False()
m3(S(0()),b,res,t) = [4] b + [4] res + [1] t + [3]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [4] b + [4] res + [1] t + [3]
>= [2]
= 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] 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.
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
gcd(x,y) -> l1(x,y,0(),False(),False(),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 DP Rules:
Weak TRS Rules:
<(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()
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:
{ [4] res + [2] t + [1] x + [1] y + [2]
= l8(x,y,res,equal0(x,y),mtmp,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()) = [0]
>= [0]
= 0()
bool2Nat(True()) = [0]
>= [0]
= S(0())
e1(a,b,res,t) = [2] 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]
>= [0]
= True()
e6(a,b,res,t) = [4] b + [2] t + [5]
>= [0]
= False()
e7(a,b,res,t) = [1] a + [1] b + [1] t + [0]
>= [0]
= False()
e8(a,b,res,t) = [2] b + [2] res + [1] t + [4]
>= [1] res + [0]
= res
equal0(a,b) = [2]
>= [0]
= e1(a,b,False(),False())
gcd(x,y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [3]
= l1(x
,y
,0()
,False()
,False()
,False())
help1(0()) = [4]
>= [0]
= False()
help1(S(0())) = [4]
>= [0]
= False()
help1(S(S(x))) = [4]
>= [0]
= True()
l1(x,y,res,tmp,mtmp,t) = [3] mtmp + [3] res + [1] t + [5] tmp + [1] x + [1] y + [3]
>= [1] mtmp + [2] res + [2] tmp + [1] x + [1] y + [3]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [1] res + [2] t + [5] tmp + [1] x + [1] y + [0]
>= [1] res + [3] tmp + [1] x + [1] y + [0]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [1] res + [3] tmp + [1] x + [1] y + [0]
>= [3] tmp + [1] x + [1] y + [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [1] res + [3] tmp + [1] x + [1] y + [0]
>= [1] tmp + [1] y + [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1] tmp + [1] y + [0]
>= [1] y + [0]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1] y + [0]
>= [1] y + [0]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [1] y + [0]
>= [1] y + [0]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [6] t + [3] tmp + [1] x + [1] y + [0]
>= [4] t + [3] tmp + [1] y + [0]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [4] t + [3] tmp + [1] y + [0]
>= [1] y + [0]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [4] t + [3] tmp + [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()) = [1] mtmp + [2] res + [2] tmp + [1] x + [1] y + [3]
>= [1] mtmp + [2] res + [2] tmp + [1] x + [1] y + [3]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1] mtmp + [2] res + [2] tmp + [1] x + [1] y + [3]
>= [1] res + [0]
= res
l3(x,y,res,tmp,mtmp,t) = [1] mtmp + [2] res + [2] t + [2] tmp + [1] x + [1] y + [3]
>= [1] mtmp + [2] t + [1] tmp + [1] x + [1] y + [3]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [1] mtmp + [7] res + [2] t + [1] tmp + [1] x + [1] x' + [3]
>= [1] mtmp + [4] res + [1] x + [1] x' + [3]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [1] mtmp + [4] res + [1] x + [1] y + [3]
>= [1] mtmp + [4] res + [1] x + [1] y + [3]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [1] mtmp + [4] res + [1] x + [1] y + [3]
>= [0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [4] mtmp + [2] tmp + [4] x + [5]
>= [0]
= 0()
l8(res,y,res',True(),mtmp,t) = [1] res + [4] res' + [2] t + [1] y + [0]
>= [1] res + [0]
= res
l8(x,y,res,False(),mtmp,t) = [4] res + [2] t + [1] x + [1] y + [0]
>= [1] res + [2] t + [1] x + [1] y + [0]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [4] mtmp + [1] res + [1] res' + [4] t + [1] tmp + [2]
>= [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()) = [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) = [4] res + [1] t + [0]
>= [0]
= False()
m3(S(0()),b,res,t) = [4] res + [1] t + [0]
>= [0]
= False()
m3(S(S(x)),b,res,t) = [4] res + [1] t + [0]
>= [0]
= True()
m4(S(x'),S(x),res,t) = [4] t + [0]
>= [1] t + [2]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [4] a + [4] b + [1] res + [1] t + [2]
>= [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.
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
<(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.
*** 1.1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
gcd(x,y) -> l1(x,y,0(),False(),False(),False())
Weak DP Rules:
Weak TRS Rules:
<(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:
{ [1 0 0] [1 0 0] [0]
[0 1 0] x + [0 1 0] y + [0]
[0 0 1] [0 0 1] [0]
= l1(x
,y
,0()
,False()
,False()
,False())
Following rules are (at-least) weakly oriented:
<(x,0()) = [0]
[1]
[0]
>= [0]
[1]
[0]
= False()
<(0(),S(y)) = [0 0 0] [0]
[0 0 0] y + [1]
[0 1 1] [1]
>= [0]
[0]
[1]
= True()
<(S(x),S(y)) = [0 0 0] [0]
[0 0 0] y + [1]
[0 1 1] [1]
>= [0 0 0] [0]
[0 0 0] y + [1]
[0 1 0] [0]
= <(x,y)
bool2Nat(False()) = [0]
[2]
[0]
>= [0]
[0]
[0]
= 0()
bool2Nat(True()) = [1]
[1]
[0]
>= [0]
[1]
[0]
= S(0())
e1(a,b,res,t) = [0 0 0] [0 0 0] [1 0
1] [0]
[1 1 1] a + [0 1 0] b + [0 0
1] res + [1]
[0 1 0] [0 0 1] [1 0
1] [0]
>= [0 0 0] [0 0 0] [1 0
1] [0]
[1 1 1] a + [0 1 0] b + [0 0
0] res + [1]
[0 1 0] [0 0 1] [0 0
0] [0]
= e2(a,b,res,<(a,b))
e2(a,b,res,False()) = [0 0 0] [0 0 0] [1 0
1] [0]
[1 1 1] a + [0 1 0] b + [0 0
0] res + [1]
[0 1 0] [0 0 1] [0 0
0] [0]
>= [0]
[1]
[0]
= False()
e2(a,b,res,True()) = [0 0 0] [0 0 0] [1 0
1] [0]
[1 1 1] a + [0 1 0] b + [0 0
0] res + [1]
[0 1 0] [0 0 1] [0 0
0] [0]
>= [0 0 0] [0 0 0] [0 0
1] [0]
[1 1 1] a + [0 0 0] b + [0 0
0] res + [1]
[0 1 0] [0 0 1] [0 0
0] [0]
= e3(a,b,res,True())
e3(a,b,res,t) = [0 0 0] [0 0 0] [0 0
1] [0]
[1 1 1] a + [0 0 0] b + [0 0
0] res + [1]
[0 1 0] [0 0 1] [0 0
0] [0]
>= [0 0 0] [0 0 0] [0]
[0 0 1] a + [0 0 0] b + [1]
[0 1 0] [0 0 1] [0]
= e4(a,b,res,<(b,a))
e4(a,b,res,False()) = [0 0 0] [0 0 0] [0]
[0 0 1] a + [0 0 0] b + [1]
[0 0 0] [0 0 1] [0]
>= [0]
[1]
[0]
= False()
e4(a,b,res,True()) = [0 0 0] [0 0 0] [0]
[0 0 1] a + [0 0 0] b + [0]
[0 0 0] [0 0 1] [1]
>= [0]
[0]
[1]
= True()
e5(a,b,res,t) = [0]
[0]
[1]
>= [0]
[0]
[1]
= True()
e6(a,b,res,t) = [1]
[1]
[1]
>= [0]
[1]
[0]
= False()
e7(a,b,res,t) = [1]
[1]
[1]
>= [0]
[1]
[0]
= False()
e8(a,b,res,t) = [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
equal0(a,b) = [0 0 0] [0 0 0] [0]
[1 1 1] a + [0 1 0] b + [1]
[0 1 0] [0 0 1] [0]
>= [0 0 0] [0 0 0] [0]
[1 1 1] a + [0 1 0] b + [1]
[0 1 0] [0 0 1] [0]
= e1(a,b,False(),False())
help1(0()) = [1]
[1]
[1]
>= [0]
[1]
[0]
= False()
help1(S(0())) = [1]
[2]
[2]
>= [0]
[1]
[0]
= False()
help1(S(S(x))) = [0 0 0] [1]
[0 1 1] x + [3]
[0 1 1] [3]
>= [0]
[0]
[1]
= True()
l1(x,y,res,tmp,mtmp,t) = [1 0 1] [1 0 0] [1
0 1] [1 0 0] [1 0
0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
0 0] tmp + [0 1 0] x + [0 1
0] y + [0]
[1 0 1] [0 1 1] [0
0 0] [0 0 1] [0 0
1] [0]
>= [1 0 1] [1 0 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [0 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [0 0 1] [0
0 1] [0 0 1] [0]
= l2(x,y,res,tmp,mtmp,False())
l10(x,y,res,tmp,mtmp,t) = [0 0 0] [0 0 0] [0
0 0] [1 0 0] [1 0
0] [0]
[1 0 0] mtmp + [0 0 0] res + [0
0 0] tmp + [0 1 0] x + [0 1
0] y + [0]
[0 0 1] [0 1 0] [0
0 1] [0 0 1] [0 0
1] [0]
>= [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[0 0 0] mtmp + [0 0 0] tmp + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 0 1] [0
0 0] [0 0 1] [0]
= l11(x,y,res,tmp,mtmp,<(x,y))
l11(x,y,res,tmp,mtmp,False()) = [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[0 0 0] mtmp + [0 0 0] tmp + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 0 1] [0
0 0] [0 0 1] [0]
>= [1 0 0] [1 0 0] [0]
[0 1 0] x + [0 1 0] y + [0]
[0 0 0] [0 0 1] [0]
= l14(x,y,res,tmp,mtmp,False())
l11(x,y,res,tmp,mtmp,True()) = [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[0 0 0] mtmp + [0 0 0] tmp + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 0 1] [0
0 0] [0 0 1] [0]
>= [1 0 0] [1 0 0] [0]
[0 0 0] x + [0 1 0] y + [0]
[0 0 0] [0 0 1] [0]
= l12(x,y,res,tmp,mtmp,True())
l12(x,y,res,tmp,mtmp,t) = [1 0 0] [1 0 0] [0]
[0 0 0] x + [0 1 0] y + [0]
[0 0 0] [0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] y + [0]
[0 0 1] [0]
= l13(x,y,res,tmp,monus(x,y),t)
l13(x,y,res,tmp,False(),t) = [1 0 0] [1]
[0 1 0] y + [0]
[0 0 1] [1]
>= [1 0 0] [1]
[0 1 0] y + [0]
[0 0 1] [1]
= l16(x
,y
,gcd(0(),y)
,tmp
,False()
,t)
l13(x,y,res,tmp,True(),t) = [1 0 0] [1]
[0 1 0] y + [1]
[0 0 1] [1]
>= [1 0 0] [1]
[0 1 0] y + [1]
[0 0 1] [1]
= l16(x
,y
,gcd(S(0()),y)
,tmp
,True()
,t)
l14(x,y,res,tmp,mtmp,t) = [0 0 1] [1 0 0] [1 0
0] [0]
[1 0 0] t + [0 1 0] x + [0 1
0] y + [0]
[0 0 1] [0 0 0] [0 0
1] [0]
>= [1 0 0] [1 0 0] [0]
[0 0 0] x + [0 1 0] y + [0]
[0 0 0] [0 0 1] [0]
= l15(x,y,res,tmp,monus(x,y),t)
l15(x,y,res,tmp,False(),t) = [1 0 0] [1 0 0] [1]
[0 0 0] x + [0 1 0] y + [0]
[0 0 0] [0 0 1] [1]
>= [1 0 0] [1]
[0 1 0] y + [0]
[0 0 1] [1]
= l16(x
,y
,gcd(y,0())
,tmp
,False()
,t)
l15(x,y,res,tmp,True(),t) = [1 0 0] [1 0 0] [1]
[0 0 0] x + [0 1 0] y + [1]
[0 0 0] [0 0 1] [1]
>= [1 0 0] [1]
[0 1 0] y + [1]
[0 0 1] [1]
= l16(x
,y
,gcd(y,S(0()))
,tmp
,True()
,t)
l16(x,y,res,tmp,mtmp,t) = [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [1]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
l2(x,y,res,tmp,mtmp,False()) = [1 0 1] [1 0 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [0 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [0 0 1] [0
0 1] [0 0 1] [0]
>= [0 0 1] [1 0 0] [1 0
0] [0]
[1 0 1] mtmp + [0 1 0] x + [0 1
0] y + [0]
[1 0 1] [0 0 1] [0 0
1] [0]
= l3(x,y,res,tmp,mtmp,False())
l2(x,y,res,tmp,mtmp,True()) = [1 0 1] [1 0 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [0 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [0 0 1] [0
0 1] [0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
l3(x,y,res,tmp,mtmp,t) = [0 0 1] [0 0 1] [1 0
0] [1 0 0] [0]
[1 0 1] mtmp + [0 0 0] t + [0 1
0] x + [0 1 0] y + [0]
[1 0 1] [1 0 0] [0 0
1] [0 0 1] [0]
>= [0 0 1] [1 0 0] [1 0
0] [0]
[1 0 1] mtmp + [0 1 0] x + [0 1
0] y + [0]
[1 0 1] [0 0 1] [0 0
1] [0]
= l4(x,y,0(),tmp,mtmp,t)
l4(x',x,res,tmp,mtmp,t) = [0 0 1] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 1] res + [0
1 0] x + [0 1 0] x' + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [0]
>= [0 0 0] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
1 0] x + [0 1 0] x' + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [0]
= l5(x',x,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,False()) = [0 0 0] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [0]
>= [0 0 0] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [0]
= l7(x,y,res,tmp,mtmp,False())
l5(x,y,res,tmp,mtmp,True()) = [0 0 0] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [1]
>= [0]
[0]
[0]
= 0()
l6(x,y,res,tmp,mtmp,t) = [0]
[0]
[1]
>= [0]
[0]
[0]
= 0()
l7(x,y,res,tmp,mtmp,t) = [0 0 0] [0 1 0] [1
0 0] [1 0 0] [0]
[1 0 1] mtmp + [1 1 0] res + [0
1 0] x + [0 1 0] y + [0]
[1 0 1] [1 1 0] [0
0 1] [0 0 1] [0]
>= [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[1 0 0] mtmp + [0 0 0] res + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 1 0] [0
0 1] [0 0 1] [0]
= l8(x,y,res,equal0(x,y),mtmp,t)
l8(res,y,res',True(),mtmp,t) = [0 0 0] [1 0 0] [0
0 0] [1 0 0] [0]
[1 0 0] mtmp + [0 1 0] res + [0
0 0] res' + [0 1 0] y + [0]
[0 0 1] [0 0 1] [0
1 0] [0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
l8(x,y,res,False(),mtmp,t) = [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[1 0 0] mtmp + [0 0 0] res + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 1 0] [0
0 1] [0 0 1] [0]
>= [0 0 0] [0 0 0] [1
0 0] [1 0 0] [0]
[1 0 0] mtmp + [0 0 0] res + [0
1 0] x + [0 1 0] y + [0]
[0 0 1] [0 1 0] [0
0 1] [0 0 1] [0]
= l10(x,y,res,False(),mtmp,t)
l9(res,y,res',tmp,mtmp,t) = [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
m1(a,x,res,t) = [0]
[0]
[0]
>= [0]
[0]
[0]
= m2(a,x,res,False())
m2(a,b,res,False()) = [0]
[0]
[0]
>= [0]
[0]
[0]
= m4(a,b,res,False())
m2(0(),b,res,True()) = [0]
[1]
[1]
>= [0]
[1]
[0]
= False()
m2(S(0()),b,res,True()) = [0]
[1]
[1]
>= [0]
[1]
[0]
= False()
m2(S(S(x)),b,res,True()) = [0]
[1]
[1]
>= [0]
[0]
[1]
= True()
m3(0(),b,res,t) = [1]
[1]
[0]
>= [0]
[1]
[0]
= False()
m3(S(0()),b,res,t) = [1]
[2]
[1]
>= [0]
[1]
[0]
= False()
m3(S(S(x)),b,res,t) = [0 0 0] [1]
[0 1 1] x + [3]
[0 1 1] [2]
>= [0]
[0]
[1]
= True()
m4(S(x'),S(x),res,t) = [0]
[0]
[0]
>= [0]
[0]
[0]
= m5(S(x'),S(x),monus(x',x),t)
m5(a,b,res,t) = [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
>= [1 0 0] [0]
[0 1 0] res + [0]
[0 0 1] [0]
= res
monus(a,b) = [0]
[0]
[0]
>= [0]
[0]
[0]
= m1(a,b,False(),False())
*** 1.1.1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(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:
{