YES Problem: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),M(x34)) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x2),x1),M(0())) -> Cons(S(x2),Cons(S(x2),x1)) scanr_cond_1(Cons(S(x20),x47),M(S(x12))) -> Cons(rec[minus_0][2](x20,x12),Cons(S(x20),x47)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](0(),x58) -> 0() rec[minus_0][2](S(x66),0()) -> S(x66) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) main(x1) -> rec[foldl_0][3](0(),rec[scanr_0][3](x1)) Proof: Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [1] [main](x0) = [1 0 1]x0 + [1] [1 1 1] [1], [1 0 1] [0] [rec[scanr_0][3]](x0) = [1 0 1]x0 + [0] [1 0 1] [1], [1 0 0] [1 0 0] [rec[plus_0][2]](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [1 0 0] [1 0 0] [1] [rec[minus_0][2]](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] [0 0 0] [0 0 0] [0], [1 0 0] [1] [M](x0) = [1 0 0]x0 + [1] [0 0 0] [0], [1 1 0] [1 1 0] [scanr_cond_1](x0, x1) = [1 1 0]x0 + [1 0 1]x1 [1 0 1] [0 0 0] , [1 0 0] [S](x0) = [0 0 0]x0 [0 0 0] , [0] [0] = [0] [0], [1 0 0] [rec[max_0][2]](x0, x1) = [0 0 0]x0 + x1 [0 0 1] , [1 1 1] [1 0 1] [Cons](x0, x1) = [1 0 0]x0 + [1 0 1]x1 [0 0 0] [1 0 1] , [1 1 0] [1 0 0] [rec[foldl_0][3]](x0, x1) = [0 1 0]x0 + [1 0 0]x1 [0 0 1] [1 0 0] , [0] [Nil] = [0] [0] orientation: [1 1 0] rec[foldl_0][3](x6,Nil()) = [0 1 0]x6 >= x6 = x6 [0 0 1] [1 1 1] [1 1 0] [1 0 1] [1 1 0] [1 0 0] [1 0 0] rec[foldl_0][3](x14,Cons(x10,x6)) = [1 1 1]x10 + [0 1 0]x14 + [1 0 1]x6 >= [0 1 0]x10 + [0 0 0]x14 + [1 0 0]x6 = rec[foldl_0][3](rec[max_0][2](x14,x10),x6) [1 1 1] [0 0 1] [1 0 1] [0 0 1] [0 0 1] [1 0 0] rec[max_0][2](0(),x26) = x26 >= x26 = x26 [1 0 0] [1 0 0] rec[max_0][2](S(x34),0()) = [0 0 0]x34 >= [0 0 0]x34 = S(x34) [0 0 0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] rec[max_0][2](S(x10),S(x6)) = [0 0 0]x10 + [0 0 0]x6 >= [0 0 0]x10 + [0 0 0]x6 = S(rec[max_0][2](x10,x6)) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [2 0 2] [2 0 2] scanr_cond_1(Cons(0(),x23),0()) = [2 0 2]x23 >= [2 0 2]x23 = Cons(0(),Cons(0(),x23)) [2 0 2] [2 0 2] [2 0 2] [2 0 0] [2 0 2] [2 0 0] scanr_cond_1(Cons(S(x34),x23),0()) = [2 0 2]x23 + [2 0 0]x34 >= [2 0 2]x23 + [2 0 0]x34 = Cons(S(x34),Cons(S(x34),x23)) [2 0 2] [1 0 0] [2 0 2] [1 0 0] [2 0 2] [2 0 0] [2] [2 0 2] scanr_cond_1(Cons(0(),x23),M(x34)) = [2 0 2]x23 + [1 0 0]x34 + [1] >= [2 0 2]x23 = Cons(0(),Cons(0(),x23)) [2 0 2] [0 0 0] [0] [2 0 2] [2 0 2] [2 0 0] [2] [2 0 2] [2 0 0] scanr_cond_1(Cons(S(x2),x1),M(0())) = [2 0 2]x1 + [2 0 0]x2 + [1] >= [2 0 2]x1 + [2 0 0]x2 = Cons(S(x2),Cons(S(x2),x1)) [2 0 2] [1 0 0] [0] [2 0 2] [1 0 0] [2 0 0] [2 0 0] [2 0 2] [2] [1 0 0] [2 0 0] [2 0 2] [1] scanr_cond_1(Cons(S(x20),x47),M(S(x12))) = [1 0 0]x12 + [2 0 0]x20 + [2 0 2]x47 + [1] >= [1 0 0]x12 + [2 0 0]x20 + [2 0 2]x47 + [1] = Cons(rec[minus_0][2](x20,x12),Cons(S(x20),x47)) [0 0 0] [1 0 0] [2 0 2] [0] [0 0 0] [1 0 0] [2 0 2] [0] [2 0 2] [1 0 0] [2 0 2] [1 0 0] scanr_cond_1(Cons(0(),x23),S(x70)) = [2 0 2]x23 + [1 0 0]x70 >= [2 0 2]x23 + [1 0 0]x70 = Cons(S(x70),Cons(0(),x23)) [2 0 2] [0 0 0] [2 0 2] [0 0 0] [1 0 0] [2 0 2] [2 0 0] [1 0 0] [2 0 2] [2 0 0] scanr_cond_1(Cons(S(x6),x23),S(x10)) = [1 0 0]x10 + [2 0 2]x23 + [2 0 0]x6 >= [1 0 0]x10 + [2 0 2]x23 + [2 0 0]x6 = Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) [0 0 0] [2 0 2] [1 0 0] [0 0 0] [2 0 2] [1 0 0] [0] [0] rec[scanr_0][3](Nil()) = [0] >= [0] = Cons(0(),Nil()) [1] [0] [1 1 1] [2 0 2] [0] [1 1 0] [2 0 2] [0] rec[scanr_0][3](Cons(x10,x6)) = [1 1 1]x10 + [2 0 2]x6 + [0] >= [1 0 1]x10 + [2 0 2]x6 + [0] = scanr_cond_1(rec[scanr_0][3](x6),x10) [1 1 1] [2 0 2] [1] [0 0 0] [2 0 2] [1] [1 0 0] [1] [0] rec[minus_0][2](0(),x58) = [0 0 0]x58 + [0] >= [0] = 0() [0 0 0] [0] [0] [1 0 0] [1] [1 0 0] rec[minus_0][2](S(x66),0()) = [0 0 0]x66 + [0] >= [0 0 0]x66 = S(x66) [0 0 0] [0] [0 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1] rec[minus_0][2](S(x10),S(x6)) = [0 0 0]x10 + [0 0 0]x6 + [0] >= [0 0 0]x10 + [0 0 0]x6 + [0] = rec[minus_0][2](x10,x6) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 0] rec[plus_0][2](0(),S(x6)) = [0 0 0]x6 >= [0 0 0]x6 = S(x6) [0 0 0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] rec[plus_0][2](S(x10),S(x6)) = [0 0 0]x10 + [0 0 0]x6 >= [0 0 0]x10 + [0 0 0]x6 = S(rec[plus_0][2](x10,S(x6))) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [1] [1 0 1] main(x1) = [1 0 1]x1 + [1] >= [1 0 1]x1 = rec[foldl_0][3](0(),rec[scanr_0][3](x1)) [1 1 1] [1] [1 0 1] problem: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) DP Processor: DPs: rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[max_0][2]#(x14,x10) rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) scanr_cond_1#(Cons(S(x6),x23),S(x10)) -> rec[plus_0][2]#(S(x10),S(x6)) rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) rec[scanr_0][3]#(Cons(x10,x6)) -> scanr_cond_1#(rec[scanr_0][3](x6),x10) rec[minus_0][2]#(S(x10),S(x6)) -> rec[minus_0][2]#(x10,x6) rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) TDG Processor: DPs: rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[max_0][2]#(x14,x10) rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) scanr_cond_1#(Cons(S(x6),x23),S(x10)) -> rec[plus_0][2]#(S(x10),S(x6)) rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) rec[scanr_0][3]#(Cons(x10,x6)) -> scanr_cond_1#(rec[scanr_0][3](x6),x10) rec[minus_0][2]#(S(x10),S(x6)) -> rec[minus_0][2]#(x10,x6) rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) graph: rec[minus_0][2]#(S(x10),S(x6)) -> rec[minus_0][2]#(x10,x6) -> rec[minus_0][2]#(S(x10),S(x6)) -> rec[minus_0][2]#(x10,x6) rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) -> rec[scanr_0][3]#(Cons(x10,x6)) -> scanr_cond_1#(rec[scanr_0][3](x6),x10) rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) -> rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) rec[scanr_0][3]#(Cons(x10,x6)) -> scanr_cond_1#(rec[scanr_0][3](x6),x10) -> scanr_cond_1#(Cons(S(x6),x23),S(x10)) -> rec[plus_0][2]#(S(x10),S(x6)) rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) -> rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) scanr_cond_1#(Cons(S(x6),x23),S(x10)) -> rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) -> rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[max_0][2]#(x14,x10) -> rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) -> rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) -> rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[max_0][2]#(x14,x10) SCC Processor: #sccs: 5 #rules: 5 #arcs: 10/64 DPs: rec[foldl_0][3]#(x14,Cons(x10,x6)) -> rec[foldl_0][3]#(rec[max_0][2](x14,x10),x6) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Subterm Criterion Processor: simple projection: pi(rec[foldl_0][3]#) = 1 problem: DPs: TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Qed DPs: rec[max_0][2]#(S(x10),S(x6)) -> rec[max_0][2]#(x10,x6) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Subterm Criterion Processor: simple projection: pi(rec[max_0][2]#) = 0 problem: DPs: TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Qed DPs: rec[scanr_0][3]#(Cons(x10,x6)) -> rec[scanr_0][3]#(x6) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Subterm Criterion Processor: simple projection: pi(rec[scanr_0][3]#) = 0 problem: DPs: TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Qed DPs: rec[plus_0][2]#(S(x10),S(x6)) -> rec[plus_0][2]#(x10,S(x6)) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Subterm Criterion Processor: simple projection: pi(rec[plus_0][2]#) = 0 problem: DPs: TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Qed DPs: rec[minus_0][2]#(S(x10),S(x6)) -> rec[minus_0][2]#(x10,x6) TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Subterm Criterion Processor: simple projection: pi(rec[minus_0][2]#) = 0 problem: DPs: TRS: rec[foldl_0][3](x6,Nil()) -> x6 rec[foldl_0][3](x14,Cons(x10,x6)) -> rec[foldl_0][3](rec[max_0][2](x14,x10),x6) rec[max_0][2](0(),x26) -> x26 rec[max_0][2](S(x34),0()) -> S(x34) rec[max_0][2](S(x10),S(x6)) -> S(rec[max_0][2](x10,x6)) scanr_cond_1(Cons(0(),x23),0()) -> Cons(0(),Cons(0(),x23)) scanr_cond_1(Cons(S(x34),x23),0()) -> Cons(S(x34),Cons(S(x34),x23)) scanr_cond_1(Cons(0(),x23),S(x70)) -> Cons(S(x70),Cons(0(),x23)) scanr_cond_1(Cons(S(x6),x23),S(x10)) -> Cons(rec[plus_0][2](S(x10),S(x6)),Cons(S(x6),x23)) rec[scanr_0][3](Nil()) -> Cons(0(),Nil()) rec[scanr_0][3](Cons(x10,x6)) -> scanr_cond_1(rec[scanr_0][3](x6),x10) rec[minus_0][2](S(x10),S(x6)) -> rec[minus_0][2](x10,x6) rec[plus_0][2](0(),S(x6)) -> S(x6) rec[plus_0][2](S(x10),S(x6)) -> S(rec[plus_0][2](x10,S(x6))) Qed