(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
m2(S(0), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0, b, res, True) → False
m3(S(0), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0, b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0
help1(S(0)) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
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)
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)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
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)
help1(0) → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0
bool2Nat(True) → S(0)
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0, tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0, False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
m4(S(x'), S(x), res, t) →+ m5(S(x'), S(x), m4(x', x, False, False), t)
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [x' / S(x'), x / S(x)].
The result substitution is [res / False, t / False].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
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)
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)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
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)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
m2(S(0'), b, res, True) → False
m2(S(S(x)), b, res, True) → True
m2(0', b, res, True) → False
m3(S(0'), b, res, t) → False
m3(S(S(x)), b, res, t) → True
m3(0', b, res, t) → False
l8(res, y, res', True, mtmp, t) → res
l5(x, y, res, tmp, mtmp, True) → 0'
help1(S(0')) → False
help1(S(S(x))) → True
e4(a, b, res, False) → False
e4(a, b, res, True) → True
e2(a, b, res, False) → False
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)
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)
m4(S(x'), S(x), res, t) → m5(S(x'), S(x), monus(x', x), t)
m2(a, b, res, False) → m4(a, b, res, False)
l8(x, y, res, False, mtmp, t) → l10(x, y, res, False, mtmp, t)
l5(x, y, res, tmp, mtmp, False) → l7(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, False) → l3(x, y, res, tmp, mtmp, False)
l2(x, y, res, tmp, mtmp, True) → res
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)
help1(0') → False
e2(a, b, res, True) → e3(a, b, res, True)
bool2Nat(False) → 0'
bool2Nat(True) → S(0')
m1(a, x, res, t) → m2(a, x, res, False)
l9(res, y, res', tmp, mtmp, t) → res
l6(x, y, res, tmp, mtmp, t) → 0'
l4(x', x, res, tmp, mtmp, t) → l5(x', x, res, tmp, mtmp, False)
l1(x, y, res, tmp, mtmp, t) → l2(x, y, res, tmp, mtmp, False)
e7(a, b, res, t) → False
e6(a, b, res, t) → False
e5(a, b, res, t) → True
monus(a, b) → m1(a, b, False, False)
m5(a, b, res, t) → res
l7(x, y, res, tmp, mtmp, t) → l8(x, y, res, equal0(x, y), mtmp, t)
l3(x, y, res, tmp, mtmp, t) → l4(x, y, 0', tmp, mtmp, t)
l16(x, y, res, tmp, mtmp, t) → res
l14(x, y, res, tmp, mtmp, t) → l15(x, y, res, tmp, monus(x, y), t)
l12(x, y, res, tmp, mtmp, t) → l13(x, y, res, tmp, monus(x, y), t)
l10(x, y, res, tmp, mtmp, t) → l11(x, y, res, tmp, mtmp, <(x, y))
gcd(x, y) → l1(x, y, 0', False, False, False)
equal0(a, b) → e1(a, b, False, False)
e8(a, b, res, t) → res
e3(a, b, res, t) → e4(a, b, res, <(b, a))
e1(a, b, res, t) → e2(a, b, res, <(a, b))
<(S(x), S(y)) → <(x, y)
<(0', S(y)) → True
<(x, 0') → False
Types:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
l15,
gcd,
l13,
m4,
monus,
m2,
l8,
l10,
l5,
l7,
l2,
l3,
l11,
l14,
l12,
l4,
<They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
< < l10
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(8) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
<, l15, gcd, l13, m4, monus, m2, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
< < l10
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
<(
gen_0':S34_17(
n36_17),
gen_0':S34_17(
+(
1,
n36_17))) →
True, rt ∈ Ω(0)
Induction Base:
<(gen_0':S34_17(0), gen_0':S34_17(+(1, 0))) →RΩ(0)
True
Induction Step:
<(gen_0':S34_17(+(n36_17, 1)), gen_0':S34_17(+(1, +(n36_17, 1)))) →RΩ(0)
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) →IH
True
We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).
(10) Complex Obligation (BEST)
(11) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
monus, l15, gcd, l13, m4, m2, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol monus.
(13) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
m2, l15, gcd, l13, m4, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol m2.
(15) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
m4, l15, gcd, l13, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
m4 = monus
m4 = m2
monus = m2
monus < l14
monus < l12
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol m4.
(17) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
gcd, l15, l13, l8, l10, l5, l7, l2, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol gcd.
(19) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l2, l15, l13, l8, l10, l5, l7, l3, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l2.
(21) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l3, l15, l13, l8, l10, l5, l7, l11, l14, l12, l4
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l3.
(23) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l4, l15, l13, l8, l10, l5, l7, l11, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l4.
(25) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l5, l15, l13, l8, l10, l7, l11, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l5.
(27) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l7, l15, l13, l8, l10, l11, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(28) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l7.
(29) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l8, l15, l13, l10, l11, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(30) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l8.
(31) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l10, l15, l13, l11, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(32) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l10.
(33) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l11, l15, l13, l14, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(34) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l11.
(35) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l14, l15, l13, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(36) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l14.
(37) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l15, l13, l12
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(38) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l15.
(39) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l12, l13
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(40) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l12.
(41) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
The following defined symbols remain to be analysed:
l13
They will be analysed ascendingly in the following order:
l15 = gcd
l15 = l13
l15 = l8
l15 = l10
l15 = l5
l15 = l7
l15 = l2
l15 = l3
l15 = l11
l15 = l14
l15 = l12
l15 = l4
gcd = l13
gcd = l8
gcd = l10
gcd = l5
gcd = l7
gcd = l2
gcd = l3
gcd = l11
gcd = l14
gcd = l12
gcd = l4
l13 = l8
l13 = l10
l13 = l5
l13 = l7
l13 = l2
l13 = l3
l13 = l11
l13 = l14
l13 = l12
l13 = l4
l8 = l10
l8 = l5
l8 = l7
l8 = l2
l8 = l3
l8 = l11
l8 = l14
l8 = l12
l8 = l4
l10 = l5
l10 = l7
l10 = l2
l10 = l3
l10 = l11
l10 = l14
l10 = l12
l10 = l4
l5 = l7
l5 = l2
l5 = l3
l5 = l11
l5 = l14
l5 = l12
l5 = l4
l7 = l2
l7 = l3
l7 = l11
l7 = l14
l7 = l12
l7 = l4
l2 = l3
l2 = l11
l2 = l14
l2 = l12
l2 = l4
l3 = l11
l3 = l14
l3 = l12
l3 = l4
l11 = l14
l11 = l12
l11 = l4
l14 = l12
l14 = l4
l12 = l4
(42) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol l13.
(43) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
No more defined symbols left to analyse.
(44) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
(45) BOUNDS(1, INF)
(46) Obligation:
Innermost TRS:
Rules:
m2(
S(
0'),
b,
res,
True) →
Falsem2(
S(
S(
x)),
b,
res,
True) →
Truem2(
0',
b,
res,
True) →
Falsem3(
S(
0'),
b,
res,
t) →
Falsem3(
S(
S(
x)),
b,
res,
t) →
Truem3(
0',
b,
res,
t) →
Falsel8(
res,
y,
res',
True,
mtmp,
t) →
resl5(
x,
y,
res,
tmp,
mtmp,
True) →
0'help1(
S(
0')) →
Falsehelp1(
S(
S(
x))) →
Truee4(
a,
b,
res,
False) →
Falsee4(
a,
b,
res,
True) →
Truee2(
a,
b,
res,
False) →
Falsel15(
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)
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)
m4(
S(
x'),
S(
x),
res,
t) →
m5(
S(
x'),
S(
x),
monus(
x',
x),
t)
m2(
a,
b,
res,
False) →
m4(
a,
b,
res,
False)
l8(
x,
y,
res,
False,
mtmp,
t) →
l10(
x,
y,
res,
False,
mtmp,
t)
l5(
x,
y,
res,
tmp,
mtmp,
False) →
l7(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
False) →
l3(
x,
y,
res,
tmp,
mtmp,
False)
l2(
x,
y,
res,
tmp,
mtmp,
True) →
resl11(
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)
help1(
0') →
Falsee2(
a,
b,
res,
True) →
e3(
a,
b,
res,
True)
bool2Nat(
False) →
0'bool2Nat(
True) →
S(
0')
m1(
a,
x,
res,
t) →
m2(
a,
x,
res,
False)
l9(
res,
y,
res',
tmp,
mtmp,
t) →
resl6(
x,
y,
res,
tmp,
mtmp,
t) →
0'l4(
x',
x,
res,
tmp,
mtmp,
t) →
l5(
x',
x,
res,
tmp,
mtmp,
False)
l1(
x,
y,
res,
tmp,
mtmp,
t) →
l2(
x,
y,
res,
tmp,
mtmp,
False)
e7(
a,
b,
res,
t) →
Falsee6(
a,
b,
res,
t) →
Falsee5(
a,
b,
res,
t) →
Truemonus(
a,
b) →
m1(
a,
b,
False,
False)
m5(
a,
b,
res,
t) →
resl7(
x,
y,
res,
tmp,
mtmp,
t) →
l8(
x,
y,
res,
equal0(
x,
y),
mtmp,
t)
l3(
x,
y,
res,
tmp,
mtmp,
t) →
l4(
x,
y,
0',
tmp,
mtmp,
t)
l16(
x,
y,
res,
tmp,
mtmp,
t) →
resl14(
x,
y,
res,
tmp,
mtmp,
t) →
l15(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l12(
x,
y,
res,
tmp,
mtmp,
t) →
l13(
x,
y,
res,
tmp,
monus(
x,
y),
t)
l10(
x,
y,
res,
tmp,
mtmp,
t) →
l11(
x,
y,
res,
tmp,
mtmp,
<(
x,
y))
gcd(
x,
y) →
l1(
x,
y,
0',
False,
False,
False)
equal0(
a,
b) →
e1(
a,
b,
False,
False)
e8(
a,
b,
res,
t) →
rese3(
a,
b,
res,
t) →
e4(
a,
b,
res,
<(
b,
a))
e1(
a,
b,
res,
t) →
e2(
a,
b,
res,
<(
a,
b))
<(
S(
x),
S(
y)) →
<(
x,
y)
<(
0',
S(
y)) →
True<(
x,
0') →
FalseTypes:
m2 :: 0':S → 0':S → True:False → True:False → True:False
S :: 0':S → 0':S
0' :: 0':S
True :: True:False
False :: True:False
m3 :: 0':S → a → b → c → True:False
l8 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l5 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
help1 :: 0':S → True:False
e4 :: 0':S → 0':S → True:False → True:False → True:False
e2 :: 0':S → 0':S → True:False → True:False → True:False
l15 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l16 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
gcd :: 0':S → 0':S → 0':S
l13 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
m4 :: 0':S → 0':S → True:False → True:False → True:False
m5 :: 0':S → 0':S → True:False → True:False → True:False
monus :: 0':S → 0':S → True:False
l10 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l7 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l2 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l3 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l11 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l14 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l12 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e3 :: 0':S → 0':S → True:False → True:False → True:False
bool2Nat :: True:False → 0':S
m1 :: 0':S → 0':S → True:False → True:False → True:False
l9 :: l9 → d → e → f → g → h → l9
l6 :: i → j → k → l → m → n → 0':S
l4 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
l1 :: 0':S → 0':S → 0':S → True:False → True:False → True:False → 0':S
e7 :: o → p → q → r → True:False
e6 :: s → t → u → v → True:False
e5 :: w → x → y → z → True:False
equal0 :: 0':S → 0':S → True:False
< :: 0':S → 0':S → True:False
e1 :: 0':S → 0':S → True:False → True:False → True:False
e8 :: za → zaa → e8 → zaaa → e8
hole_True:False1_17 :: True:False
hole_0':S2_17 :: 0':S
hole_a3_17 :: a
hole_b4_17 :: b
hole_c5_17 :: c
hole_l96_17 :: l9
hole_d7_17 :: d
hole_e8_17 :: e
hole_f9_17 :: f
hole_g10_17 :: g
hole_h11_17 :: h
hole_i12_17 :: i
hole_j13_17 :: j
hole_k14_17 :: k
hole_l15_17 :: l
hole_m16_17 :: m
hole_n17_17 :: n
hole_o18_17 :: o
hole_p19_17 :: p
hole_q20_17 :: q
hole_r21_17 :: r
hole_s22_17 :: s
hole_t23_17 :: t
hole_u24_17 :: u
hole_v25_17 :: v
hole_w26_17 :: w
hole_x27_17 :: x
hole_y28_17 :: y
hole_z29_17 :: z
hole_e830_17 :: e8
hole_za31_17 :: za
hole_zaa32_17 :: zaa
hole_zaaa33_17 :: zaaa
gen_0':S34_17 :: Nat → 0':S
Lemmas:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
Generator Equations:
gen_0':S34_17(0) ⇔ 0'
gen_0':S34_17(+(x, 1)) ⇔ S(gen_0':S34_17(x))
No more defined symbols left to analyse.
(47) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(1) was proven with the following lemma:
<(gen_0':S34_17(n36_17), gen_0':S34_17(+(1, n36_17))) → True, rt ∈ Ω(0)
(48) BOUNDS(1, INF)