YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(true,true) -> true,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false,
     ordered(cons(?x,cons(s(?x),nil))) -> true,
     ordered(cons(s(?x),cons(?x,nil))) -> false ]
Constructors: {0,s,nil,cons,true,false}
Defined function symbols: {le,and,ordered,leList}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
   [ and(true,true) -> true,
     ordered(cons(?x,cons(s(?x),nil))) -> true,
     ordered(cons(s(?x),cons(?x,nil))) -> false ]
Trying with:
R:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
E:
   [ and(true,true) = true,
     ordered(cons(?x,cons(s(?x),nil))) = true,
     ordered(cons(s(?x),cons(?x,nil))) = false ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool,List}
Signature:
   [ ordered : List -> Bool,
     leList : Nat,List -> Bool,
     le : Nat,Nat -> Bool,
     and : Bool,Bool -> Bool,
     cons : Nat,List -> List,
     true : Bool,
     false : Bool,
     nil : List,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
Conjecture Part:
   [ and(true,true) = true,
     ordered(cons(?x,cons(s(?x),nil))) = true,
     ordered(cons(s(?x),cons(?x,nil))) = false ]
Precedence (by weight): {(0,0),(s,10),(le,12),(and,11),(nil,13),(cons,9),(true,4),(ordered,15),(false,3),(leList,14)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false ]
Conjectures:
   [ and(true,true) = true,
     ordered(cons(?x,cons(s(?x),nil))) = true,
     ordered(cons(s(?x),cons(?x,nil))) = false ]
STEP 0
ES:
   [ and(true,true) = true,
     ordered(cons(?x,cons(s(?x),nil))) = true,
     ordered(cons(s(?x),cons(?x,nil))) = false ]
HS:
   [ ]
ES0:
   [ true = true,
     le(?x,s(?x)) = true,
     le(s(?x),?x) = false ]
HS0:
   [ ]
ES1:
   [ le(?x,s(?x)) = true,
     le(s(?x),?x) = false ]
HS1:
   [ ]
Expand le(?x,s(?x)) = true
   [ true = true,
     le(?x_6,s(?x_6)) = true ]
ES2:
   [ true = true,
     le(?x_6,s(?x_6)) = true,
     le(s(?x),?x) = false ]
HS2:
   [ le(?x,s(?x)) -> true ]
STEP 1
ES:
   [ true = true,
     le(?x_6,s(?x_6)) = true,
     le(s(?x),?x) = false ]
HS:
   [ le(?x,s(?x)) -> true ]
ES0:
   [ true = true,
     true = true,
     le(s(?x),?x) = false ]
HS0:
   [ le(?x,s(?x)) -> true ]
ES1:
   [ le(s(?x),?x) = false ]
HS1:
   [ le(?x,s(?x)) -> true ]
Expand le(s(?x),?x) = false
   [ false = false,
     le(s(?y_6),?y_6) = false ]
ES2:
   [ false = false,
     le(s(?y_6),?y_6) = false ]
HS2:
   [ le(s(?x),?x) -> false,
     le(?x,s(?x)) -> true ]
STEP 2
ES:
   [ false = false,
     le(s(?y_6),?y_6) = false ]
HS:
   [ le(s(?x),?x) -> false,
     le(?x,s(?x)) -> true ]
ES0:
   [ false = false,
     false = false ]
HS0:
   [ le(s(?x),?x) -> false,
     le(?x,s(?x)) -> true ]
ES1:
   [ ]
HS1:
   [ le(s(?x),?x) -> false,
     le(?x,s(?x)) -> true ]
Conj part consisits of inductive theorems of R0.
new/ordered.trs: Success(GCR)
(46 msec.)