MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     f(0) -> 0,
     f(?x) -> if(zero(?x),s(0),0) ]
Constructors: {0,s,true,false}
Defined function symbols: {f,if,zero}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     f(?x) -> if(zero(?x),s(0),0) ]
   [ f(0) -> 0 ]
Trying with:
R:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     f(?x) -> if(zero(?x),s(0),0) ]
E:
   [ f(0) = 0 ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ zero : Nat -> Bool,
     if : Bool,Nat,Nat -> Nat,
     f : Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat,
     true : Bool,
     false : Bool ]
Rule Part:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     f(?x) -> if(zero(?x),s(0),0) ]
Conjecture Part:
   [ f(0) = 0 ]
Precedence (by weight): {(0,4),(f,7),(s,3),(if,1),(true,0),(zero,5),(false,2)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     f(?x) -> if(zero(?x),s(0),0) ]
Conjectures:
   [ f(0) = 0 ]
STEP 0
ES:
   [ f(0) = 0 ]
HS:
   [ ]
ES0:
   [ s(0) = 0 ]
HS0:
   [ ]
ES1:
   [ s(0) = 0 ]
HS1:
   [ ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
new/gncr.trs: Failure(unknown)
(184 msec.)