YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     max(0,?y) -> ?y,
     max(?x,0) -> ?x,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     le(min(?x,?y),max(?x,?y)) -> true,
     min(?x,?y) -> min(?y,?x),
     max(?x,?y) -> max(?y,?x) ]
Constructors: {0,s,true,false}
Defined function symbols: {le,max,min}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     max(0,?y) -> ?y,
     max(?x,0) -> ?x,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y) ]
   [ le(min(?x,?y),max(?x,?y)) -> true,
     min(?x,?y) -> min(?y,?x),
     max(?x,?y) -> max(?y,?x) ]
Trying with:
R:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     max(0,?y) -> ?y,
     max(?x,0) -> ?x,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y) ]
E:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ min : Nat,Nat -> Nat,
     max : Nat,Nat -> Nat,
     le : Nat,Nat -> Bool,
     true : Bool,
     false : Bool,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     max(0,?y) -> ?y,
     max(?x,0) -> ?x,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y) ]
Conjecture Part:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
Precedence (by weight): {(0,6),(s,1),(le,0),(max,3),(min,2),(true,5),(false,4)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     max(0,?y) -> ?y,
     max(?x,0) -> ?x,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y) ]
Conjectures:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
STEP 0
ES:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
HS:
   [ ]
ES0:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
HS0:
   [ ]
ES1:
   [ le(min(?x,?y),max(?x,?y)) = true,
     min(?x,?y) = min(?y,?x),
     max(?x,?y) = max(?y,?x) ]
HS1:
   [ ]
Expand min(?x,?y) = min(?y,?x)
   [ 0 = min(?y_1,0),
     0 = min(0,?x_2),
     s(min(?x_3,?y_3)) = min(s(?y_3),s(?x_3)) ]
ES2:
   [ 0 = min(?y_1,0),
     0 = min(0,?x_2),
     s(min(?x_3,?y_3)) = min(s(?y_3),s(?x_3)),
     max(?x,?y) = max(?y,?x),
     le(min(?x,?y),max(?x,?y)) = true ]
HS2:
   [ min(?x,?y) -> min(?y,?x) ]
STEP 1
ES:
   [ 0 = min(?y_1,0),
     0 = min(0,?x_2),
     s(min(?x_3,?y_3)) = min(s(?y_3),s(?x_3)),
     max(?x,?y) = max(?y,?x),
     le(min(?x,?y),max(?x,?y)) = true ]
HS:
   [ min(?x,?y) -> min(?y,?x) ]
ES0:
   [ 0 = 0,
     0 = 0,
     s(min(?x_3,?y_3)) = s(min(?y_3,?x_3)),
     max(?x,?y) = max(?y,?x),
     le(min(?x,?y),max(?x,?y)) = true ]
HS0:
   [ min(?x,?y) -> min(?y,?x) ]
ES1:
   [ max(?x,?y) = max(?y,?x),
     le(min(?x,?y),max(?x,?y)) = true ]
HS1:
   [ min(?x,?y) -> min(?y,?x) ]
Expand max(?x,?y) = max(?y,?x)
   [ ?y_4 = max(?y_4,0),
     ?x_5 = max(0,?x_5),
     s(max(?x_6,?y_6)) = max(s(?y_6),s(?x_6)) ]
ES2:
   [ ?y_4 = max(?y_4,0),
     ?x_5 = max(0,?x_5),
     s(max(?x_6,?y_6)) = max(s(?y_6),s(?x_6)),
     le(min(?x,?y),max(?x,?y)) = true ]
HS2:
   [ max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
STEP 2
ES:
   [ ?y_4 = max(?y_4,0),
     ?x_5 = max(0,?x_5),
     s(max(?x_6,?y_6)) = max(s(?y_6),s(?x_6)),
     le(min(?x,?y),max(?x,?y)) = true ]
HS:
   [ max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
ES0:
   [ ?y_4 = ?y_4,
     ?x_5 = ?x_5,
     s(max(?x_6,?y_6)) = s(max(?y_6,?x_6)),
     le(min(?x,?y),max(?x,?y)) = true ]
HS0:
   [ max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
ES1:
   [ le(min(?x,?y),max(?x,?y)) = true ]
HS1:
   [ max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
Expand le(min(?x,?y),max(?x,?y)) = true
   [ le(0,max(0,?y_1)) = true,
     le(0,max(?x_2,0)) = true,
     le(s(min(?x_3,?y_3)),max(s(?x_3),s(?y_3))) = true ]
ES2:
   [ true = true,
     true = true,
     le(min(?x_3,?y_3),max(?x_3,?y_3)) = true ]
HS2:
   [ le(min(?x,?y),max(?x,?y)) -> true,
     max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
STEP 3
ES:
   [ true = true,
     true = true,
     le(min(?x_3,?y_3),max(?x_3,?y_3)) = true ]
HS:
   [ le(min(?x,?y),max(?x,?y)) -> true,
     max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
ES0:
   [ true = true,
     true = true,
     le(min(?x_3,?y_3),max(?x_3,?y_3)) = true ]
HS0:
   [ le(min(?x,?y),max(?x,?y)) -> true,
     max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
ES1:
   [ ]
HS1:
   [ le(min(?x,?y),max(?x,?y)) -> true,
     max(?x,?y) -> max(?y,?x),
     min(?x,?y) -> min(?y,?x) ]
Conj part consisits of inductive theorems of R0.
new/min-max.trs: Success(GCR)
(37 msec.)