YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(round(?xs)) -> len(?xs) ]
Constructors: {0,s,nil,cons}
Defined function symbols: {app,len,round}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)) ]
   [ len(round(?xs)) -> len(?xs) ]
Trying with:
R:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)) ]
E:
   [ len(round(?xs)) = len(?xs) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,List}
Signature:
   [ len : List -> Nat,
     round : List -> List,
     app : List,List -> List,
     cons : Nat,List -> List,
     nil : List,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)) ]
Conjecture Part:
   [ len(round(?xs)) = len(?xs) ]
Precedence (by weight): {(0,0),(s,2),(app,5),(len,7),(nil,4),(cons,3),(round,6)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     round(nil) -> nil,
     round(cons(?x,?xs)) -> app(?xs,cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)) ]
Conjectures:
   [ len(round(?xs)) = len(?xs) ]
STEP 0
ES:
   [ len(round(?xs)) = len(?xs) ]
HS:
   [ ]
ES0:
   [ len(round(?xs)) = len(?xs) ]
HS0:
   [ ]
ES1:
   [ len(round(?xs)) = len(?xs) ]
HS1:
   [ ]
Expand len(round(?xs)) = len(?xs)
   [ len(nil) = len(nil),
     len(app(?xs_2,cons(?x_2,nil))) = len(cons(?x_2,?xs_2)) ]
ES2:
   [ 0 = len(nil),
     len(app(?xs_2,cons(?x_2,nil))) = len(cons(?x_2,?xs_2)) ]
HS2:
   [ len(round(?xs)) -> len(?xs) ]
STEP 1
ES:
   [ 0 = len(nil),
     len(app(?xs_2,cons(?x_2,nil))) = len(cons(?x_2,?xs_2)) ]
HS:
   [ len(round(?xs)) -> len(?xs) ]
ES0:
   [ 0 = 0,
     len(app(?xs_2,cons(?x_2,nil))) = s(len(?xs_2)) ]
HS0:
   [ len(round(?xs)) -> len(?xs) ]
ES1:
   [ len(app(?xs_2,cons(?x_2,nil))) = s(len(?xs_2)) ]
HS1:
   [ len(round(?xs)) -> len(?xs) ]
Expand len(app(?xs_2,cons(?x_2,nil))) = s(len(?xs_2))
   [ len(cons(?x,nil)) = s(len(nil)),
     len(cons(?x_4,app(?xs_4,cons(?x,nil)))) = s(len(cons(?x_4,?xs_4))) ]
ES2:
   [ s(0) = s(len(nil)),
     s(len(app(?xs_4,cons(?x,nil)))) = s(len(cons(?x_4,?xs_4))) ]
HS2:
   [ len(app(?xs_2,cons(?x_2,nil))) -> s(len(?xs_2)),
     len(round(?xs)) -> len(?xs) ]
STEP 2
ES:
   [ s(0) = s(len(nil)),
     s(len(app(?xs_4,cons(?x,nil)))) = s(len(cons(?x_4,?xs_4))) ]
HS:
   [ len(app(?xs_2,cons(?x_2,nil))) -> s(len(?xs_2)),
     len(round(?xs)) -> len(?xs) ]
ES0:
   [ s(0) = s(0),
     s(s(len(?xs_4))) = s(s(len(?xs_4))) ]
HS0:
   [ len(app(?xs_2,cons(?x_2,nil))) -> s(len(?xs_2)),
     len(round(?xs)) -> len(?xs) ]
ES1:
   [ ]
HS1:
   [ len(app(?xs_2,cons(?x_2,nil))) -> s(len(?xs_2)),
     len(round(?xs)) -> len(?xs) ]
Conj part consisits of inductive theorems of R0.
new/len-round.trs: Success(GCR)
(18 msec.)