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