YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     sum(mirror(?xt)) -> sum(?xt) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,leaf,node}
Defined function symbols: {+,sum,mirror}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ sum(mirror(?xt)) -> sum(?xt) ]
Trying with:
R:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
E:
   [ sum(mirror(?xt)) = sum(?xt) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Tree}
Signature:
   [ mirror : Tree -> Tree,
     leaf : Nat -> Tree,
     node : Nat,Tree,Tree -> Tree,
     sum : Tree -> Nat,
     + : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjecture Part:
   [ sum(mirror(?xt)) = sum(?xt) ]
Precedence (by weight): {(+,3),(0,2),(s,0),(sum,4),(leaf,1),(node,5),(mirror,6)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ mirror(leaf(?x)) -> leaf(?x),
     mirror(node(?x,?yt,?zt)) -> node(?x,mirror(?zt),mirror(?yt)),
     sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(sum(?yt),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Conjectures:
   [ sum(mirror(?xt)) = sum(?xt) ]
STEP 0
ES:
   [ sum(mirror(?xt)) = sum(?xt) ]
HS:
   [ ]
ES0:
   [ sum(mirror(?xt)) = sum(?xt) ]
HS0:
   [ ]
ES1:
   [ sum(mirror(?xt)) = sum(?xt) ]
HS1:
   [ ]
Expand sum(mirror(?xt)) = sum(?xt)
   [ sum(leaf(?x_1)) = sum(leaf(?x_1)),
     sum(node(?x_2,mirror(?zt_2),mirror(?yt_2))) = sum(node(?x_2,?yt_2,?zt_2)) ]
ES2:
   [ ?x_1 = sum(leaf(?x_1)),
     +(sum(mirror(?zt_2)),sum(mirror(?yt_2))) = sum(node(?x_2,?yt_2,?zt_2)) ]
HS2:
   [ sum(mirror(?xt)) -> sum(?xt) ]
STEP 1
ES:
   [ ?x_1 = sum(leaf(?x_1)),
     +(sum(mirror(?zt_2)),sum(mirror(?yt_2))) = sum(node(?x_2,?yt_2,?zt_2)) ]
HS:
   [ sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ ?x_1 = ?x_1,
     +(sum(?zt_2),sum(?yt_2)) = +(sum(?yt_2),sum(?zt_2)) ]
HS0:
   [ sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ +(sum(?zt_2),sum(?yt_2)) = +(sum(?yt_2),sum(?zt_2)) ]
HS1:
   [ sum(mirror(?xt)) -> sum(?xt) ]
Expand +(sum(?zt_2),sum(?yt_2)) = +(sum(?yt_2),sum(?zt_2))
   [ +(?x_3,sum(?yt)) = +(sum(?yt),sum(leaf(?x_3))),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),sum(node(?x_4,?yt_4,?zt_4))) ]
ES2:
   [ +(?x_3,sum(?yt)) = +(sum(?yt),sum(leaf(?x_3))),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),sum(node(?x_4,?yt_4,?zt_4))) ]
HS2:
   [ +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
STEP 2
ES:
   [ +(?x_3,sum(?yt)) = +(sum(?yt),sum(leaf(?x_3))),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),sum(node(?x_4,?yt_4,?zt_4))) ]
HS:
   [ +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ +(?x_3,sum(?yt)) = +(sum(?yt),?x_3),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),+(sum(?yt_4),sum(?zt_4))) ]
HS0:
   [ +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ +(?x_3,sum(?yt)) = +(sum(?yt),?x_3),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),+(sum(?yt_4),sum(?zt_4))) ]
HS1:
   [ +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
Expand +(?x_3,sum(?yt)) = +(sum(?yt),?x_3)
   [ +(?x_3,?x_6) = +(sum(leaf(?x_6)),?x_3),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(sum(node(?x_7,?yt_7,?zt_7)),?x_3) ]
ES2:
   [ +(?x_3,?x_6) = +(sum(leaf(?x_6)),?x_3),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(sum(node(?x_7,?yt_7,?zt_7)),?x_3),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),+(sum(?yt_4),sum(?zt_4))) ]
HS2:
   [ +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
STEP 3
ES:
   [ +(?x_3,?x_6) = +(sum(leaf(?x_6)),?x_3),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(sum(node(?x_7,?yt_7,?zt_7)),?x_3),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),+(sum(?yt_4),sum(?zt_4))) ]
HS:
   [ +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ +(?x_3,?x_6) = +(?x_6,?x_3),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(+(sum(?yt_7),sum(?zt_7)),?x_3),
     +(+(sum(?yt_4),sum(?zt_4)),sum(?yt)) = +(sum(?yt),+(sum(?yt_4),sum(?zt_4))) ]
HS0:
   [ +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ +(?x_3,?x_6) = +(?x_6,?x_3),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(+(sum(?yt_7),sum(?zt_7)),?x_3) ]
HS1:
   [ +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
Expand +(?x_3,?x_6) = +(?x_6,?x_3)
   [ ?y_8 = +(?y_8,0),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
ES2:
   [ ?y_8 = +(?y_8,0),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(+(sum(?yt_7),sum(?zt_7)),?x_3) ]
HS2:
   [ +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
STEP 4
ES:
   [ ?y_8 = +(?y_8,0),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(+(sum(?yt_7),sum(?zt_7)),?x_3) ]
HS:
   [ +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ ?y_8 = +(?y_8,0),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)),
     +(?x_3,+(sum(?yt_7),sum(?zt_7))) = +(+(sum(?yt_7),sum(?zt_7)),?x_3) ]
HS0:
   [ +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ ?y_8 = +(?y_8,0),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
HS1:
   [ +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
Expand +(?y_8,0) = ?y_8
   [ 0 = 0,
     s(+(?x_6,0)) = s(?x_6) ]
ES2:
   [ 0 = 0,
     s(+(?x_6,0)) = s(?x_6),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
HS2:
   [ +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
STEP 5
ES:
   [ 0 = 0,
     s(+(?x_6,0)) = s(?x_6),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
HS:
   [ +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ 0 = 0,
     s(?x_6) = s(?x_6),
     s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
HS0:
   [ +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ s(+(?x_9,?y_9)) = +(?y_9,s(?x_9)) ]
HS1:
   [ +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
Expand +(?y_9,s(?x_9)) = s(+(?x_9,?y_9))
   [ s(?x) = s(+(?x,0)),
     s(+(?x_6,s(?x))) = s(+(?x,s(?x_6))) ]
ES2:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_6,s(?x))) = s(+(?x,s(?x_6))) ]
HS2:
   [ +(?y_9,s(?x_9)) -> s(+(?x_9,?y_9)),
     +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
STEP 6
ES:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_6,s(?x))) = s(+(?x,s(?x_6))) ]
HS:
   [ +(?y_9,s(?x_9)) -> s(+(?x_9,?y_9)),
     +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES0:
   [ s(?x) = s(?x),
     s(s(+(?x,?x_6))) = s(s(+(?x_6,?x))) ]
HS0:
   [ +(?y_9,s(?x_9)) -> s(+(?x_9,?y_9)),
     +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
ES1:
   [ ]
HS1:
   [ +(?y_9,s(?x_9)) -> s(+(?x_9,?y_9)),
     +(?y_8,0) -> ?y_8,
     +(?x_3,?x_6) -> +(?x_6,?x_3),
     +(?x_3,sum(?yt)) -> +(sum(?yt),?x_3),
     +(sum(?zt_2),sum(?yt_2)) -> +(sum(?yt_2),sum(?zt_2)),
     sum(mirror(?xt)) -> sum(?xt) ]
Conj part consisits of inductive theorems of R0.
new/mirror.trs: Success(GCR)
(1779 msec.)