YES(?,O(n^1)) TRS: { f X -> n__f X, f n__f n__a() -> f n__g f n__a(), g X -> n__g X, a() -> n__a(), activate X -> X, activate n__g X -> g X, activate n__a() -> a(), activate n__f X -> f X } DUP: We consider a non-duplicating system. Trs: { f X -> n__f X, f n__f n__a() -> f n__g f n__a(), g X -> n__g X, a() -> n__a(), activate X -> X, activate n__g X -> g X, activate n__a() -> a(), activate n__f X -> f X } RLAB: Strict: { f(f) f(f) X -> f(n__f) n__f(f) X, f(f) f(n__f) X -> f(n__f) n__f(n__f) X, f(f) f(g) X -> f(n__f) n__f(g) X, f(f) f(n__g) X -> f(n__f) n__f(n__g) X, f(f) f(n__a) X -> f(n__f) n__f(n__a) X, f(f) f(a) X -> f(n__f) n__f(a) X, f(f) f(activate) X -> f(n__f) n__f(activate) X, f(n__f) n__f(n__a) n__a() -> f(n__g) n__g(f) f(n__a) n__a(), f(g) g(f) X -> f(n__g) n__g(f) X, f(g) g(n__f) X -> f(n__g) n__g(n__f) X, f(g) g(g) X -> f(n__g) n__g(g) X, f(g) g(n__g) X -> f(n__g) n__g(n__g) X, f(g) g(n__a) X -> f(n__g) n__g(n__a) X, f(g) g(a) X -> f(n__g) n__g(a) X, f(g) g(activate) X -> f(n__g) n__g(activate) X, f(a) a() -> f(n__a) n__a(), f(activate) activate(f) X -> f(f) X, f(activate) activate(n__f) X -> f(n__f) X, f(activate) activate(n__f) n__f(f) X -> f(f) f(f) X, f(activate) activate(n__f) n__f(n__f) X -> f(f) f(n__f) X, f(activate) activate(n__f) n__f(g) X -> f(f) f(g) X, f(activate) activate(n__f) n__f(n__g) X -> f(f) f(n__g) X, f(activate) activate(n__f) n__f(n__a) X -> f(f) f(n__a) X, f(activate) activate(n__f) n__f(a) X -> f(f) f(a) X, f(activate) activate(n__f) n__f(activate) X -> f(f) f(activate) X, f(activate) activate(g) X -> f(g) X, f(activate) activate(n__g) X -> f(n__g) X, f(activate) activate(n__g) n__g(f) X -> f(g) g(f) X, f(activate) activate(n__g) n__g(n__f) X -> f(g) g(n__f) X, f(activate) activate(n__g) n__g(g) X -> f(g) g(g) X, f(activate) activate(n__g) n__g(n__g) X -> f(g) g(n__g) X, f(activate) activate(n__g) n__g(n__a) X -> f(g) g(n__a) X, f(activate) activate(n__g) n__g(a) X -> f(g) g(a) X, f(activate) activate(n__g) n__g(activate) X -> f(g) g(activate) X, f(activate) activate(n__a) X -> f(n__a) X, f(activate) activate(n__a) n__a() -> f(a) a(), f(activate) activate(a) X -> f(a) X, f(activate) activate(activate) X -> f(activate) X, g(f) f(f) X -> g(n__f) n__f(f) X, g(f) f(n__f) X -> g(n__f) n__f(n__f) X, g(f) f(g) X -> g(n__f) n__f(g) X, g(f) f(n__g) X -> g(n__f) n__f(n__g) X, g(f) f(n__a) X -> g(n__f) n__f(n__a) X, g(f) f(a) X -> g(n__f) n__f(a) X, g(f) f(activate) X -> g(n__f) n__f(activate) X, g(g) g(f) X -> g(n__g) n__g(f) X, g(g) g(n__f) X -> g(n__g) n__g(n__f) X, g(g) g(g) X -> g(n__g) n__g(g) X, g(g) g(n__g) X -> g(n__g) n__g(n__g) X, g(g) g(n__a) X -> g(n__g) n__g(n__a) X, g(g) g(a) X -> g(n__g) n__g(a) X, g(g) g(activate) X -> g(n__g) n__g(activate) X, g(a) a() -> g(n__a) n__a(), g(activate) activate(f) X -> g(f) X, g(activate) activate(n__f) X -> g(n__f) X, g(activate) activate(n__f) n__f(f) X -> g(f) f(f) X, g(activate) activate(n__f) n__f(n__f) X -> g(f) f(n__f) X, g(activate) activate(n__f) n__f(g) X -> g(f) f(g) X, g(activate) activate(n__f) n__f(n__g) X -> g(f) f(n__g) X, g(activate) activate(n__f) n__f(n__a) X -> g(f) f(n__a) X, g(activate) activate(n__f) n__f(a) X -> g(f) f(a) X, g(activate) activate(n__f) n__f(activate) X -> g(f) f(activate) X, g(activate) activate(g) X -> g(g) X, g(activate) activate(n__g) X -> g(n__g) X, g(activate) activate(n__g) n__g(f) X -> g(g) g(f) X, g(activate) activate(n__g) n__g(n__f) X -> g(g) g(n__f) X, g(activate) activate(n__g) n__g(g) X -> g(g) g(g) X, g(activate) activate(n__g) n__g(n__g) X -> g(g) g(n__g) X, g(activate) activate(n__g) n__g(n__a) X -> g(g) g(n__a) X, g(activate) activate(n__g) n__g(a) X -> g(g) g(a) X, g(activate) activate(n__g) n__g(activate) X -> g(g) g(activate) X, g(activate) activate(n__a) X -> g(n__a) X, g(activate) activate(n__a) n__a() -> g(a) a(), g(activate) activate(a) X -> g(a) X, g(activate) activate(activate) X -> g(activate) X, n__g(f) f(f) X -> n__g(n__f) n__f(f) X, n__g(f) f(n__f) X -> n__g(n__f) n__f(n__f) X, n__g(f) f(g) X -> n__g(n__f) n__f(g) X, n__g(f) f(n__g) X -> n__g(n__f) n__f(n__g) X, n__g(f) f(n__a) X -> n__g(n__f) n__f(n__a) X, n__g(f) f(a) X -> n__g(n__f) n__f(a) X, n__g(f) f(activate) X -> n__g(n__f) n__f(activate) X, n__g(g) g(f) X -> n__g(n__g) n__g(f) X, n__g(g) g(n__f) X -> n__g(n__g) n__g(n__f) X, n__g(g) g(g) X -> n__g(n__g) n__g(g) X, n__g(g) g(n__g) X -> n__g(n__g) n__g(n__g) X, n__g(g) g(n__a) X -> n__g(n__g) n__g(n__a) X, n__g(g) g(a) X -> n__g(n__g) n__g(a) X, n__g(g) g(activate) X -> n__g(n__g) n__g(activate) X, n__g(a) a() -> n__g(n__a) n__a(), n__g(activate) activate(f) X -> n__g(f) X, n__g(activate) activate(n__f) X -> n__g(n__f) X, n__g(activate) activate(n__f) n__f(f) X -> n__g(f) f(f) X, n__g(activate) activate(n__f) n__f(n__f) X -> n__g(f) f(n__f) X, n__g(activate) activate(n__f) n__f(g) X -> n__g(f) f(g) X, n__g(activate) activate(n__f) n__f(n__g) X -> n__g(f) f(n__g) X, n__g(activate) activate(n__f) n__f(n__a) X -> n__g(f) f(n__a) X, n__g(activate) activate(n__f) n__f(a) X -> n__g(f) f(a) X, n__g(activate) activate(n__f) n__f(activate) X -> n__g(f) f(activate) X, n__g(activate) activate(g) X -> n__g(g) X, n__g(activate) activate(n__g) X -> n__g(n__g) X, n__g(activate) activate(n__g) n__g(f) X -> n__g(g) g(f) X, n__g(activate) activate(n__g) n__g(n__f) X -> n__g(g) g(n__f) X, n__g(activate) activate(n__g) n__g(g) X -> n__g(g) g(g) X, n__g(activate) activate(n__g) n__g(n__g) X -> n__g(g) g(n__g) X, n__g(activate) activate(n__g) n__g(n__a) X -> n__g(g) g(n__a) X, n__g(activate) activate(n__g) n__g(a) X -> n__g(g) g(a) X, n__g(activate) activate(n__g) n__g(activate) X -> n__g(g) g(activate) X, n__g(activate) activate(n__a) X -> n__g(n__a) X, n__g(activate) activate(n__a) n__a() -> n__g(a) a(), n__g(activate) activate(a) X -> n__g(a) X, n__g(activate) activate(activate) X -> n__g(activate) X, n__f(f) f(f) X -> n__f(n__f) n__f(f) X, n__f(f) f(n__f) X -> n__f(n__f) n__f(n__f) X, n__f(f) f(g) X -> n__f(n__f) n__f(g) X, n__f(f) f(n__g) X -> n__f(n__f) n__f(n__g) X, n__f(f) f(n__a) X -> n__f(n__f) n__f(n__a) X, n__f(f) f(a) X -> n__f(n__f) n__f(a) X, n__f(f) f(activate) X -> n__f(n__f) n__f(activate) X, n__f(g) g(f) X -> n__f(n__g) n__g(f) X, n__f(g) g(n__f) X -> n__f(n__g) n__g(n__f) X, n__f(g) g(g) X -> n__f(n__g) n__g(g) X, n__f(g) g(n__g) X -> n__f(n__g) n__g(n__g) X, n__f(g) g(n__a) X -> n__f(n__g) n__g(n__a) X, n__f(g) g(a) X -> n__f(n__g) n__g(a) X, n__f(g) g(activate) X -> n__f(n__g) n__g(activate) X, n__f(a) a() -> n__f(n__a) n__a(), n__f(activate) activate(f) X -> n__f(f) X, n__f(activate) activate(n__f) X -> n__f(n__f) X, n__f(activate) activate(n__f) n__f(f) X -> n__f(f) f(f) X, n__f(activate) activate(n__f) n__f(n__f) X -> n__f(f) f(n__f) X, n__f(activate) activate(n__f) n__f(g) X -> n__f(f) f(g) X, n__f(activate) activate(n__f) n__f(n__g) X -> n__f(f) f(n__g) X, n__f(activate) activate(n__f) n__f(n__a) X -> n__f(f) f(n__a) X, n__f(activate) activate(n__f) n__f(a) X -> n__f(f) f(a) X, n__f(activate) activate(n__f) n__f(activate) X -> n__f(f) f(activate) X, n__f(activate) activate(g) X -> n__f(g) X, n__f(activate) activate(n__g) X -> n__f(n__g) X, n__f(activate) activate(n__g) n__g(f) X -> n__f(g) g(f) X, n__f(activate) activate(n__g) n__g(n__f) X -> n__f(g) g(n__f) X, n__f(activate) activate(n__g) n__g(g) X -> n__f(g) g(g) X, n__f(activate) activate(n__g) n__g(n__g) X -> n__f(g) g(n__g) X, n__f(activate) activate(n__g) n__g(n__a) X -> n__f(g) g(n__a) X, n__f(activate) activate(n__g) n__g(a) X -> n__f(g) g(a) X, n__f(activate) activate(n__g) n__g(activate) X -> n__f(g) g(activate) X, n__f(activate) activate(n__a) X -> n__f(n__a) X, n__f(activate) activate(n__a) n__a() -> n__f(a) a(), n__f(activate) activate(a) X -> n__f(a) X, n__f(activate) activate(activate) X -> n__f(activate) X, activate(f) f(f) X -> activate(n__f) n__f(f) X, activate(f) f(n__f) X -> activate(n__f) n__f(n__f) X, activate(f) f(g) X -> activate(n__f) n__f(g) X, activate(f) f(n__g) X -> activate(n__f) n__f(n__g) X, activate(f) f(n__a) X -> activate(n__f) n__f(n__a) X, activate(f) f(a) X -> activate(n__f) n__f(a) X, activate(f) f(activate) X -> activate(n__f) n__f(activate) X, activate(g) g(f) X -> activate(n__g) n__g(f) X, activate(g) g(n__f) X -> activate(n__g) n__g(n__f) X, activate(g) g(g) X -> activate(n__g) n__g(g) X, activate(g) g(n__g) X -> activate(n__g) n__g(n__g) X, activate(g) g(n__a) X -> activate(n__g) n__g(n__a) X, activate(g) g(a) X -> activate(n__g) n__g(a) X, activate(g) g(activate) X -> activate(n__g) n__g(activate) X, activate(a) a() -> activate(n__a) n__a(), activate(activate) activate(f) X -> activate(f) X, activate(activate) activate(n__f) X -> activate(n__f) X, activate(activate) activate(n__f) n__f(f) X -> activate(f) f(f) X, activate(activate) activate(n__f) n__f(n__f) X -> activate(f) f(n__f) X, activate(activate) activate(n__f) n__f(g) X -> activate(f) f(g) X, activate(activate) activate(n__f) n__f(n__g) X -> activate(f) f(n__g) X, activate(activate) activate(n__f) n__f(n__a) X -> activate(f) f(n__a) X, activate(activate) activate(n__f) n__f(a) X -> activate(f) f(a) X, activate(activate) activate(n__f) n__f(activate) X -> activate(f) f(activate) X, activate(activate) activate(g) X -> activate(g) X, activate(activate) activate(n__g) X -> activate(n__g) X, activate(activate) activate(n__g) n__g(f) X -> activate(g) g(f) X, activate(activate) activate(n__g) n__g(n__f) X -> activate(g) g(n__f) X, activate(activate) activate(n__g) n__g(g) X -> activate(g) g(g) X, activate(activate) activate(n__g) n__g(n__g) X -> activate(g) g(n__g) X, activate(activate) activate(n__g) n__g(n__a) X -> activate(g) g(n__a) X, activate(activate) activate(n__g) n__g(a) X -> activate(g) g(a) X, activate(activate) activate(n__g) n__g(activate) X -> activate(g) g(activate) X, activate(activate) activate(n__a) X -> activate(n__a) X, activate(activate) activate(n__a) n__a() -> activate(a) a(), activate(activate) activate(a) X -> activate(a) X, activate(activate) activate(activate) X -> activate(activate) X } Weak: {} Natural interpretation: Strict: { f(f) f(f) X -> f(n__f) n__f(f) X, f(f) f(n__f) X -> f(n__f) n__f(n__f) X, f(f) f(g) X -> f(n__f) n__f(g) X, f(f) f(n__g) X -> f(n__f) n__f(n__g) X, f(f) f(n__a) X -> f(n__f) n__f(n__a) X, f(f) f(a) X -> f(n__f) n__f(a) X, f(f) f(activate) X -> f(n__f) n__f(activate) X, f(n__f) n__f(n__a) n__a() -> f(n__g) n__g(f) f(n__a) n__a(), f(g) g(f) X -> f(n__g) n__g(f) X, f(g) g(n__f) X -> f(n__g) n__g(n__f) X, f(g) g(g) X -> f(n__g) n__g(g) X, f(g) g(n__g) X -> f(n__g) n__g(n__g) X, f(g) g(n__a) X -> f(n__g) n__g(n__a) X, f(g) g(a) X -> f(n__g) n__g(a) X, f(g) g(activate) X -> f(n__g) n__g(activate) X, f(a) a() -> f(n__a) n__a(), f(activate) activate(f) X -> f(f) X, f(activate) activate(n__f) X -> f(n__f) X, f(activate) activate(n__f) n__f(f) X -> f(f) f(f) X, f(activate) activate(n__f) n__f(n__f) X -> f(f) f(n__f) X, f(activate) activate(n__f) n__f(g) X -> f(f) f(g) X, f(activate) activate(n__f) n__f(n__g) X -> f(f) f(n__g) X, f(activate) activate(n__f) n__f(n__a) X -> f(f) f(n__a) X, f(activate) activate(n__f) n__f(a) X -> f(f) f(a) X, f(activate) activate(n__f) n__f(activate) X -> f(f) f(activate) X, f(activate) activate(g) X -> f(g) X, f(activate) activate(n__g) X -> f(n__g) X, f(activate) activate(n__g) n__g(f) X -> f(g) g(f) X, f(activate) activate(n__g) n__g(n__f) X -> f(g) g(n__f) X, f(activate) activate(n__g) n__g(g) X -> f(g) g(g) X, f(activate) activate(n__g) n__g(n__g) X -> f(g) g(n__g) X, f(activate) activate(n__g) n__g(n__a) X -> f(g) g(n__a) X, f(activate) activate(n__g) n__g(a) X -> f(g) g(a) X, f(activate) activate(n__g) n__g(activate) X -> f(g) g(activate) X, f(activate) activate(n__a) X -> f(n__a) X, f(activate) activate(n__a) n__a() -> f(a) a(), f(activate) activate(a) X -> f(a) X, f(activate) activate(activate) X -> f(activate) X, g(f) f(f) X -> g(n__f) n__f(f) X, g(f) f(n__f) X -> g(n__f) n__f(n__f) X, g(f) f(g) X -> g(n__f) n__f(g) X, g(f) f(n__g) X -> g(n__f) n__f(n__g) X, g(f) f(n__a) X -> g(n__f) n__f(n__a) X, g(f) f(a) X -> g(n__f) n__f(a) X, g(f) f(activate) X -> g(n__f) n__f(activate) X, g(g) g(f) X -> g(n__g) n__g(f) X, g(g) g(n__f) X -> g(n__g) n__g(n__f) X, g(g) g(g) X -> g(n__g) n__g(g) X, g(g) g(n__g) X -> g(n__g) n__g(n__g) X, g(g) g(n__a) X -> g(n__g) n__g(n__a) X, g(g) g(a) X -> g(n__g) n__g(a) X, g(g) g(activate) X -> g(n__g) n__g(activate) X, g(a) a() -> g(n__a) n__a(), g(activate) activate(f) X -> g(f) X, g(activate) activate(n__f) X -> g(n__f) X, g(activate) activate(n__f) n__f(f) X -> g(f) f(f) X, g(activate) activate(n__f) n__f(n__f) X -> g(f) f(n__f) X, g(activate) activate(n__f) n__f(g) X -> g(f) f(g) X, g(activate) activate(n__f) n__f(n__g) X -> g(f) f(n__g) X, g(activate) activate(n__f) n__f(n__a) X -> g(f) f(n__a) X, g(activate) activate(n__f) n__f(a) X -> g(f) f(a) X, g(activate) activate(n__f) n__f(activate) X -> g(f) f(activate) X, g(activate) activate(g) X -> g(g) X, g(activate) activate(n__g) X -> g(n__g) X, g(activate) activate(n__g) n__g(f) X -> g(g) g(f) X, g(activate) activate(n__g) n__g(n__f) X -> g(g) g(n__f) X, g(activate) activate(n__g) n__g(g) X -> g(g) g(g) X, g(activate) activate(n__g) n__g(n__g) X -> g(g) g(n__g) X, g(activate) activate(n__g) n__g(n__a) X -> g(g) g(n__a) X, g(activate) activate(n__g) n__g(a) X -> g(g) g(a) X, g(activate) activate(n__g) n__g(activate) X -> g(g) g(activate) X, g(activate) activate(n__a) X -> g(n__a) X, g(activate) activate(n__a) n__a() -> g(a) a(), g(activate) activate(a) X -> g(a) X, g(activate) activate(activate) X -> g(activate) X, n__g(f) f(f) X -> n__g(n__f) n__f(f) X, n__g(f) f(n__f) X -> n__g(n__f) n__f(n__f) X, n__g(f) f(g) X -> n__g(n__f) n__f(g) X, n__g(f) f(n__g) X -> n__g(n__f) n__f(n__g) X, n__g(f) f(n__a) X -> n__g(n__f) n__f(n__a) X, n__g(f) f(a) X -> n__g(n__f) n__f(a) X, n__g(f) f(activate) X -> n__g(n__f) n__f(activate) X, n__g(g) g(f) X -> n__g(n__g) n__g(f) X, n__g(g) g(n__f) X -> n__g(n__g) n__g(n__f) X, n__g(g) g(g) X -> n__g(n__g) n__g(g) X, n__g(g) g(n__g) X -> n__g(n__g) n__g(n__g) X, n__g(g) g(n__a) X -> n__g(n__g) n__g(n__a) X, n__g(g) g(a) X -> n__g(n__g) n__g(a) X, n__g(g) g(activate) X -> n__g(n__g) n__g(activate) X, n__g(a) a() -> n__g(n__a) n__a(), n__g(activate) activate(f) X -> n__g(f) X, n__g(activate) activate(n__f) X -> n__g(n__f) X, n__g(activate) activate(n__f) n__f(f) X -> n__g(f) f(f) X, n__g(activate) activate(n__f) n__f(n__f) X -> n__g(f) f(n__f) X, n__g(activate) activate(n__f) n__f(g) X -> n__g(f) f(g) X, n__g(activate) activate(n__f) n__f(n__g) X -> n__g(f) f(n__g) X, n__g(activate) activate(n__f) n__f(n__a) X -> n__g(f) f(n__a) X, n__g(activate) activate(n__f) n__f(a) X -> n__g(f) f(a) X, n__g(activate) activate(n__f) n__f(activate) X -> n__g(f) f(activate) X, n__g(activate) activate(g) X -> n__g(g) X, n__g(activate) activate(n__g) X -> n__g(n__g) X, n__g(activate) activate(n__g) n__g(f) X -> n__g(g) g(f) X, n__g(activate) activate(n__g) n__g(n__f) X -> n__g(g) g(n__f) X, n__g(activate) activate(n__g) n__g(g) X -> n__g(g) g(g) X, n__g(activate) activate(n__g) n__g(n__g) X -> n__g(g) g(n__g) X, n__g(activate) activate(n__g) n__g(n__a) X -> n__g(g) g(n__a) X, n__g(activate) activate(n__g) n__g(a) X -> n__g(g) g(a) X, n__g(activate) activate(n__g) n__g(activate) X -> n__g(g) g(activate) X, n__g(activate) activate(n__a) X -> n__g(n__a) X, n__g(activate) activate(n__a) n__a() -> n__g(a) a(), n__g(activate) activate(a) X -> n__g(a) X, n__g(activate) activate(activate) X -> n__g(activate) X, n__f(f) f(f) X -> n__f(n__f) n__f(f) X, n__f(f) f(n__f) X -> n__f(n__f) n__f(n__f) X, n__f(f) f(g) X -> n__f(n__f) n__f(g) X, n__f(f) f(n__g) X -> n__f(n__f) n__f(n__g) X, n__f(f) f(n__a) X -> n__f(n__f) n__f(n__a) X, n__f(f) f(a) X -> n__f(n__f) n__f(a) X, n__f(f) f(activate) X -> n__f(n__f) n__f(activate) X, n__f(g) g(f) X -> n__f(n__g) n__g(f) X, n__f(g) g(n__f) X -> n__f(n__g) n__g(n__f) X, n__f(g) g(g) X -> n__f(n__g) n__g(g) X, n__f(g) g(n__g) X -> n__f(n__g) n__g(n__g) X, n__f(g) g(n__a) X -> n__f(n__g) n__g(n__a) X, n__f(g) g(a) X -> n__f(n__g) n__g(a) X, n__f(g) g(activate) X -> n__f(n__g) n__g(activate) X, n__f(a) a() -> n__f(n__a) n__a(), n__f(activate) activate(f) X -> n__f(f) X, n__f(activate) activate(n__f) X -> n__f(n__f) X, n__f(activate) activate(n__f) n__f(f) X -> n__f(f) f(f) X, n__f(activate) activate(n__f) n__f(n__f) X -> n__f(f) f(n__f) X, n__f(activate) activate(n__f) n__f(g) X -> n__f(f) f(g) X, n__f(activate) activate(n__f) n__f(n__g) X -> n__f(f) f(n__g) X, n__f(activate) activate(n__f) n__f(n__a) X -> n__f(f) f(n__a) X, n__f(activate) activate(n__f) n__f(a) X -> n__f(f) f(a) X, n__f(activate) activate(n__f) n__f(activate) X -> n__f(f) f(activate) X, n__f(activate) activate(g) X -> n__f(g) X, n__f(activate) activate(n__g) X -> n__f(n__g) X, n__f(activate) activate(n__g) n__g(f) X -> n__f(g) g(f) X, n__f(activate) activate(n__g) n__g(n__f) X -> n__f(g) g(n__f) X, n__f(activate) activate(n__g) n__g(g) X -> n__f(g) g(g) X, n__f(activate) activate(n__g) n__g(n__g) X -> n__f(g) g(n__g) X, n__f(activate) activate(n__g) n__g(n__a) X -> n__f(g) g(n__a) X, n__f(activate) activate(n__g) n__g(a) X -> n__f(g) g(a) X, n__f(activate) activate(n__g) n__g(activate) X -> n__f(g) g(activate) X, n__f(activate) activate(n__a) X -> n__f(n__a) X, n__f(activate) activate(n__a) n__a() -> n__f(a) a(), n__f(activate) activate(a) X -> n__f(a) X, n__f(activate) activate(activate) X -> n__f(activate) X, activate(f) f(f) X -> activate(n__f) n__f(f) X, activate(f) f(n__f) X -> activate(n__f) n__f(n__f) X, activate(f) f(g) X -> activate(n__f) n__f(g) X, activate(f) f(n__g) X -> activate(n__f) n__f(n__g) X, activate(f) f(n__a) X -> activate(n__f) n__f(n__a) X, activate(f) f(a) X -> activate(n__f) n__f(a) X, activate(f) f(activate) X -> activate(n__f) n__f(activate) X, activate(g) g(f) X -> activate(n__g) n__g(f) X, activate(g) g(n__f) X -> activate(n__g) n__g(n__f) X, activate(g) g(g) X -> activate(n__g) n__g(g) X, activate(g) g(n__g) X -> activate(n__g) n__g(n__g) X, activate(g) g(n__a) X -> activate(n__g) n__g(n__a) X, activate(g) g(a) X -> activate(n__g) n__g(a) X, activate(g) g(activate) X -> activate(n__g) n__g(activate) X, activate(a) a() -> activate(n__a) n__a(), activate(activate) activate(f) X -> activate(f) X, activate(activate) activate(n__f) X -> activate(n__f) X, activate(activate) activate(n__f) n__f(f) X -> activate(f) f(f) X, activate(activate) activate(n__f) n__f(n__f) X -> activate(f) f(n__f) X, activate(activate) activate(n__f) n__f(g) X -> activate(f) f(g) X, activate(activate) activate(n__f) n__f(n__g) X -> activate(f) f(n__g) X, activate(activate) activate(n__f) n__f(n__a) X -> activate(f) f(n__a) X, activate(activate) activate(n__f) n__f(a) X -> activate(f) f(a) X, activate(activate) activate(n__f) n__f(activate) X -> activate(f) f(activate) X, activate(activate) activate(g) X -> activate(g) X, activate(activate) activate(n__g) X -> activate(n__g) X, activate(activate) activate(n__g) n__g(f) X -> activate(g) g(f) X, activate(activate) activate(n__g) n__g(n__f) X -> activate(g) g(n__f) X, activate(activate) activate(n__g) n__g(g) X -> activate(g) g(g) X, activate(activate) activate(n__g) n__g(n__g) X -> activate(g) g(n__g) X, activate(activate) activate(n__g) n__g(n__a) X -> activate(g) g(n__a) X, activate(activate) activate(n__g) n__g(a) X -> activate(g) g(a) X, activate(activate) activate(n__g) n__g(activate) X -> activate(g) g(activate) X, activate(activate) activate(n__a) X -> activate(n__a) X, activate(activate) activate(n__a) n__a() -> activate(a) a(), activate(activate) activate(a) X -> activate(a) X, activate(activate) activate(activate) X -> activate(activate) X } Weak: {} Interpretation class: stronglylinear [activate(6)](X0) = + 1*X0 + 6 [activate(5)](X0) = + 1*X0 + 0 [activate(4)](X0) = + 1*X0 + 4 [activate(3)](X0) = + 1*X0 + 2 [activate(2)](X0) = + 1*X0 + 6 [activate(1)](X0) = + 1*X0 + 1 [activate(0)](X0) = + 1*X0 + 6 [a] = + 7 [n__f(6)](X0) = + 1*X0 + 7 [n__f(5)](X0) = + 1*X0 + 1 [n__f(4)](X0) = + 1*X0 + 3 [n__f(3)](X0) = + 1*X0 + 1 [n__f(2)](X0) = + 1*X0 + 3 [n__f(1)](X0) = + 1*X0 + 3 [n__f(0)](X0) = + 1*X0 + 7 [n__a] = + 1 [n__g(6)](X0) = + 1*X0 + 5 [n__g(5)](X0) = + 1*X0 + 1 [n__g(4)](X0) = + 1*X0 + 3 [n__g(3)](X0) = + 1*X0 + 2 [n__g(2)](X0) = + 1*X0 + 5 [n__g(1)](X0) = + 1*X0 + 0 [n__g(0)](X0) = + 1*X0 + 5 [g(6)](X0) = + 1*X0 + 6 [g(5)](X0) = + 1*X0 + 0 [g(4)](X0) = + 1*X0 + 4 [g(3)](X0) = + 1*X0 + 3 [g(2)](X0) = + 1*X0 + 6 [g(1)](X0) = + 1*X0 + 0 [g(0)](X0) = + 1*X0 + 4 [f(6)](X0) = + 1*X0 + 7 [f(5)](X0) = + 1*X0 + 1 [f(4)](X0) = + 1*X0 + 0 [f(3)](X0) = + 1*X0 + 0 [f(2)](X0) = + 1*X0 + 2 [f(1)](X0) = + 1*X0 + 3 [f(0)](X0) = + 1*X0 + 7 Qed