*** 1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__zeros()) -> zeros() tail(cons(X,XS)) -> activate(XS) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() Weak DP Rules: Weak TRS Rules: Signature: {activate/1,tail/1,zeros/0} / {0/0,cons/2,n__zeros/0} Obligation: Full basic terms: {activate,tail,zeros}/{0,cons,n__zeros} Applied Processor: ToInnermost Proof: switch to innermost, as the system is overlay and right linear and does not contain weak rules *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: activate(X) -> X activate(n__zeros()) -> zeros() tail(cons(X,XS)) -> activate(XS) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() Weak DP Rules: Weak TRS Rules: Signature: {activate/1,tail/1,zeros/0} / {0/0,cons/2,n__zeros/0} Obligation: Innermost basic terms: {activate,tail,zeros}/{0,cons,n__zeros} Applied Processor: DependencyPairs {dpKind_ = DT} Proof: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__zeros()) -> c_2(zeros#()) tail#(cons(X,XS)) -> c_3(activate#(XS)) zeros#() -> c_4() zeros#() -> c_5() Weak DPs and mark the set of starting terms. *** 1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: activate#(X) -> c_1() activate#(n__zeros()) -> c_2(zeros#()) tail#(cons(X,XS)) -> c_3(activate#(XS)) zeros#() -> c_4() zeros#() -> c_5() Strict TRS Rules: Weak DP Rules: Weak TRS Rules: activate(X) -> X activate(n__zeros()) -> zeros() tail(cons(X,XS)) -> activate(XS) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() Signature: {activate/1,tail/1,zeros/0,activate#/1,tail#/1,zeros#/0} / {0/0,cons/2,n__zeros/0,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0} Obligation: Innermost basic terms: {activate#,tail#,zeros#}/{0,cons,n__zeros} Applied Processor: UsableRules Proof: We replace rewrite rules by usable rules: activate#(X) -> c_1() activate#(n__zeros()) -> c_2(zeros#()) tail#(cons(X,XS)) -> c_3(activate#(XS)) zeros#() -> c_4() zeros#() -> c_5() *** 1.1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: activate#(X) -> c_1() activate#(n__zeros()) -> c_2(zeros#()) tail#(cons(X,XS)) -> c_3(activate#(XS)) zeros#() -> c_4() zeros#() -> c_5() Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {activate/1,tail/1,zeros/0,activate#/1,tail#/1,zeros#/0} / {0/0,cons/2,n__zeros/0,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0} Obligation: Innermost basic terms: {activate#,tail#,zeros#}/{0,cons,n__zeros} Applied Processor: Trivial Proof: Consider the dependency graph 1:S:activate#(X) -> c_1() 2:S:activate#(n__zeros()) -> c_2(zeros#()) -->_1 zeros#() -> c_5():5 -->_1 zeros#() -> c_4():4 3:S:tail#(cons(X,XS)) -> c_3(activate#(XS)) -->_1 activate#(n__zeros()) -> c_2(zeros#()):2 -->_1 activate#(X) -> c_1():1 4:S:zeros#() -> c_4() 5:S:zeros#() -> c_5() The dependency graph contains no loops, we remove all dependency pairs. *** 1.1.1.1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: Signature: {activate/1,tail/1,zeros/0,activate#/1,tail#/1,zeros#/0} / {0/0,cons/2,n__zeros/0,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0} Obligation: Innermost basic terms: {activate#,tail#,zeros#}/{0,cons,n__zeros} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).