U11(tt, V1, V2) → U12(isNat(activate(V1)), activate(V2))
U12(tt, V2) → U13(isNat(activate(V2)))
U13(tt) → tt
U21(tt, V1) → U22(isNat(activate(V1)))
U22(tt) → tt
U31(tt, V1, V2) → U32(isNat(activate(V1)), activate(V2))
U32(tt, V2) → U33(isNat(activate(V2)))
U33(tt) → tt
U41(tt, N) → activate(N)
U51(tt, M, N) → s(plus(activate(N), activate(M)))
U61(tt) → 0
U71(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)) → U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNat(n__x(V1, V2)) → U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1), activate(V2))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) → isNatKind(activate(V1))
isNatKind(n__x(V1, V2)) → and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
plus(N, 0) → U41(and(isNat(N), n__isNatKind(N)), N)
plus(N, s(M)) → U51(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)
x(N, 0) → U61(and(isNat(N), n__isNatKind(N)))
x(N, s(M)) → U71(and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
isNatKind(X) → n__isNatKind(X)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
and(X1, X2) → n__and(X1, X2)
isNat(X) → n__isNat(X)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(activate(X1), activate(X2))
activate(n__isNatKind(X)) → isNatKind(X)
activate(n__s(X)) → s(activate(X))
activate(n__x(X1, X2)) → x(activate(X1), activate(X2))
activate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isNat(X)) → isNat(X)
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', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Infered types.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Heuristically decided to analyse the following defined symbols:
isNat', activate', U41', plus', x', and', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
and', isNat', activate', U41', plus', x', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol and'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
activate', isNat', U41', plus', x', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Proved the following rewrite lemma:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Induction Base:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, 0)))
Induction Step:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, +(_$n56569, 1)))) →RΩ(1)
plus'(activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _$n56569))), activate'(tt')) →IH
plus'(_*3, activate'(tt')) →RΩ(1)
plus'(_*3, tt')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
plus', isNat', U41', x', and', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol plus'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
U41', isNat', x', and', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol U41'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
isNat', x', and', isNatKind'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol isNat'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
isNatKind', x', and'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol isNatKind'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
x', and'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol x'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
The following defined symbols remain to be analysed:
and'
They will be analysed ascendingly in the following order:
isNat' = activate'
isNat' = U41'
isNat' = plus'
isNat' = x'
isNat' = and'
isNat' = isNatKind'
activate' = U41'
activate' = plus'
activate' = x'
activate' = and'
activate' = isNatKind'
U41' = plus'
U41' = x'
U41' = and'
U41' = isNatKind'
plus' = x'
plus' = and'
plus' = isNatKind'
x' = and'
x' = isNatKind'
and' = isNatKind'
Could not prove a rewrite lemma for the defined symbol and'.
Rules:
U11'(tt', V1, V2) → U12'(isNat'(activate'(V1)), activate'(V2))
U12'(tt', V2) → U13'(isNat'(activate'(V2)))
U13'(tt') → tt'
U21'(tt', V1) → U22'(isNat'(activate'(V1)))
U22'(tt') → tt'
U31'(tt', V1, V2) → U32'(isNat'(activate'(V1)), activate'(V2))
U32'(tt', V2) → U33'(isNat'(activate'(V2)))
U33'(tt') → tt'
U41'(tt', N) → activate'(N)
U51'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U61'(tt') → 0'
U71'(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)) → U11'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNat'(n__s'(V1)) → U21'(isNatKind'(activate'(V1)), activate'(V1))
isNat'(n__x'(V1, V2)) → U31'(and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2))), activate'(V1), activate'(V2))
isNatKind'(n__0') → tt'
isNatKind'(n__plus'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
isNatKind'(n__s'(V1)) → isNatKind'(activate'(V1))
isNatKind'(n__x'(V1, V2)) → and'(isNatKind'(activate'(V1)), n__isNatKind'(activate'(V2)))
plus'(N, 0') → U41'(and'(isNat'(N), n__isNatKind'(N)), N)
plus'(N, s'(M)) → U51'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
x'(N, 0') → U61'(and'(isNat'(N), n__isNatKind'(N)))
x'(N, s'(M)) → U71'(and'(and'(isNat'(M), n__isNatKind'(M)), n__and'(n__isNat'(N), n__isNatKind'(N))), M, N)
0' → n__0'
plus'(X1, X2) → n__plus'(X1, X2)
isNatKind'(X) → n__isNatKind'(X)
s'(X) → n__s'(X)
x'(X1, X2) → n__x'(X1, X2)
and'(X1, X2) → n__and'(X1, X2)
isNat'(X) → n__isNat'(X)
activate'(n__0') → 0'
activate'(n__plus'(X1, X2)) → plus'(activate'(X1), activate'(X2))
activate'(n__isNatKind'(X)) → isNatKind'(X)
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__x'(X1, X2)) → x'(activate'(X1), activate'(X2))
activate'(n__and'(X1, X2)) → and'(activate'(X1), X2)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
U11' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
tt' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U12' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
activate' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U13' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U21' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U22' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U31' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U32' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U33' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U41' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U51' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U61' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
U71' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__0' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__plus' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNatKind' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__s' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__x' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__and' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
n__isNat' :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and' → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_hole_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'1 :: tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2 :: Nat → tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'
Lemmas:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)
Generator Equations:
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(0) ⇔ tt'
_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(x, 1)) ⇔ n__plus'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(x), tt')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_tt':n__0':n__plus':n__isNatKind':n__s':n__x':n__isNat':n__and'2(+(1, _n56568))) → _*3, rt ∈ Ω(n56568)