MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,?y) -> +(?y,?x),
     node(?x,?yt,?zt) -> node(?x,?zt,?yt) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,leaf,node}
Defined function symbols: {+,sum}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ +(?x,?y) -> +(?y,?x),
     node(?x,?yt,?zt) -> node(?x,?zt,?yt) ]
Trying with:
R:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
E:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Tree}
Signature:
   [ + : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat,
     node : Nat,Tree,Tree -> Tree,
     leaf : Nat -> Tree,
     sum : Tree -> Nat ]
Rule Part:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
Precedence (by weight): {(+,5),(0,1),(s,4),(sum,2),(leaf,3),(node,6)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjectures:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
STEP 0
ES:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS:
   [ ]
ES0:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS0:
   [ ]
ES1:
   [ +(?x,?y) = +(?y,?x),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS1:
   [ ]
Expand +(?x,?y) = +(?y,?x)
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)) ]
ES2:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS2:
   [ +(?x,?y) -> +(?y,?x) ]
STEP 1
ES:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS:
   [ +(?x,?y) -> +(?y,?x) ]
ES0:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS0:
   [ +(?x,?y) -> +(?y,?x) ]
ES1:
   [ ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS1:
   [ +(?x,?y) -> +(?y,?x) ]
Expand +(?y_3,0) = ?y_3
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4) ]
ES2:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     node(?x,?yt,?zt) = node(?x,?zt,?yt),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)) ]
HS2:
   [ +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
STEP 2
ES:
   [ 0 = 0,
     s(+(?x_4,0)) = s(?x_4),
     node(?x,?yt,?zt) = node(?x,?zt,?yt),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)) ]
HS:
   [ +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ 0 = 0,
     s(?x_4) = s(?x_4),
     node(?x,?yt,?zt) = node(?x,?zt,?yt),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)) ]
HS0:
   [ +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ node(?x,?yt,?zt) = node(?x,?zt,?yt),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)) ]
HS1:
   [ +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
Expand +(?y_4,s(?x_4)) = s(+(?x_4,?y_4))
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))) ]
ES2:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS2:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
STEP 3
ES:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_4,s(?x))) = s(+(?x,s(?x_4))),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ s(?x) = s(?x),
     s(s(+(?x,?x_4))) = s(s(+(?x_4,?x))),
     node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS0:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ node(?x,?yt,?zt) = node(?x,?zt,?yt) ]
HS1:
   [ +(?y_4,s(?x_4)) -> s(+(?x_4,?y_4)),
     +(?y_3,0) -> ?y_3,
     +(?x,?y) -> +(?y,?x) ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
new/tree6.trs: Failure(unknown)
(1763 msec.)