U11(tt, N) → activate(N)
U21(tt, M, N) → s(plus(activate(N), activate(M)))
U31(tt) → 0
U41(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
isNat(n__s(V1)) → isNat(activate(V1))
isNat(n__x(V1, V2)) → and(isNat(activate(V1)), n__isNat(activate(V2)))
plus(N, 0) → U11(isNat(N), N)
plus(N, s(M)) → U21(and(isNat(M), n__isNat(N)), M, N)
x(N, 0) → U31(isNat(N))
x(N, s(M)) → U41(and(isNat(M), n__isNat(N)), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNat(X) → n__isNat(X)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__isNat(X)) → isNat(X)
activate(n__s(X)) → s(X)
activate(n__x(X1, X2)) → x(X1, X2)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Infered types.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Heuristically decided to analyse the following defined symbols:
U11', activate', plus', x', and', isNat'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
activate', U11', plus', x', and', isNat'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
plus', U11', x', and', isNat'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol plus'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
U11', x', and', isNat'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol U11'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
isNat', x', and'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Proved the following rewrite lemma:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Induction Base:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, 0)))
Induction Step:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, +(_$n636, 1)))) →RΩ(1)
and'(isNat'(activate'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _$n636)))), n__isNat'(activate'(tt'))) →RΩ(1)
and'(isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _$n636))), n__isNat'(activate'(tt'))) →IH
and'(_*3, n__isNat'(activate'(tt'))) →RΩ(1)
and'(_*3, n__isNat'(tt'))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
and', U11', activate', plus', x'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol and'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
x', U11', activate', plus'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol x'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
activate', U11', plus'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
plus', U11'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol plus'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
The following defined symbols remain to be analysed:
U11'
They will be analysed ascendingly in the following order:
U11' = activate'
U11' = plus'
U11' = x'
U11' = and'
U11' = isNat'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNat'
plus' = x'
plus' = and'
plus' = isNat'
x' = and'
x' = isNat'
and' = isNat'
Could not prove a rewrite lemma for the defined symbol U11'.
Rules:
U11'(tt', N) → activate'(N)
U21'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U31'(tt') → 0'
U41'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__plus'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNat'(n__x'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNat'(activate'(V2)))
plus'(N, 0') → U11'(isNat'(N), N)
plus'(N, s'(M)) → U21'(and'(isNat'(M), n__isNat'(N)), M, N)
x'(N, 0') → U31'(isNat'(N))
x'(N, s'(M)) → U41'(and'(isNat'(M), n__isNat'(N)), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNat'(X) → n__isNat'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(X1, X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(n__s'(X)) → s'(X)
activate'(n__x'(X1, X2)) → x'(X1, X2)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
tt' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
activate' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U21' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
U31' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
U41' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
and' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__0' :: tt':n__0':n__plus':n__isNat':n__s':n__x'
n__plus' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__isNat' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__s' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
n__x' :: tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x' → tt':n__0':n__plus':n__isNat':n__s':n__x'
_hole_tt':n__0':n__plus':n__isNat':n__s':n__x'1 :: tt':n__0':n__plus':n__isNat':n__s':n__x'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2 :: Nat → tt':n__0':n__plus':n__isNat':n__s':n__x'
Lemmas:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(x), tt')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
isNat'(_gen_tt':n__0':n__plus':n__isNat':n__s':n__x'2(+(1, _n635))) → _*3, rt ∈ Ω(n635)