YES
(ignored inputs)COMMENT [Friburg , JSC 1989] Example p.225
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ le(0,?x) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Constructors: {0,s,true,false}
Defined function symbols: {+,le}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ le(0,?x) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ le : Nat,Nat -> Bool,
     true : Bool,
     false : Bool,
     + : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ le(0,?x) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ ]
Precedence (by weight): {(+,6),(0,0),(s,5),(le,3),(true,1),(false,2)}
Rule part is confluent.
R0 is ground confluent.
Conjucture part is empty.
examples/additions/le1.trs: Success(GCR)
(18 msec.)