MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> min(?x,?y),
     min(?x,?x) -> ?x ]
Constructors: {0,s}
Defined function symbols: {min}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> min(?x,?y) ]
   [ min(?x,?x) -> ?x ]
Trying with:
R:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> min(?x,?y) ]
E:
   [ min(?x,?x) = ?x ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ min : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> min(?x,?y) ]
Conjecture Part:
   [ min(?x,?x) = ?x ]
Precedence (by weight): {(0,0),(s,1),(min,2)}
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)) -> min(?x,?y) ]
Conjectures:
   [ min(?x,?x) = ?x ]
STEP 0
ES:
   [ min(?x,?x) = ?x ]
HS:
   [ ]
ES0:
   [ min(?x,?x) = ?x ]
HS0:
   [ ]
ES1:
   [ min(?x,?x) = ?x ]
HS1:
   [ ]
Expand min(?x,?x) = ?x
   [ 0 = 0,
     0 = 0,
     min(?y_3,?y_3) = s(?y_3) ]
ES2:
   [ 0 = 0,
     0 = 0,
     min(?y_3,?y_3) = s(?y_3) ]
HS2:
   [ min(?x,?x) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     0 = 0,
     min(?y_3,?y_3) = s(?y_3) ]
HS:
   [ min(?x,?x) -> ?x ]
ES0:
   [ 0 = 0,
     0 = 0,
     ?y_3 = s(?y_3) ]
HS0:
   [ min(?x,?x) -> ?x ]
ES1:
   [ ?y_3 = s(?y_3) ]
HS1:
   [ min(?x,?x) -> ?x ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
new/min5.trs: Failure(unknown)
(11 msec.)