NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty y z x)
(REPLACEMENT-MAP
(+ 1, 2)
(br 1, 2, 3)
(p 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
+(x,y) -> br(y,x,+(s(x),p(y)))
+(x,y) -> br(x,y,+(p(x),s(y)))
br(0,y,z) -> y
br(s(x),y,z) -> z
p(0) -> 0
p(s(x)) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty y z x)
(REPLACEMENT-MAP
(+ 1, 2)
(br 1, 2, 3)
(p 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
+(x,y) -> br(y,x,+(s(x),p(y)))
+(x,y) -> br(x,y,+(p(x),s(y)))
br(0,y,z) -> y
br(s(x),y,z) -> z
p(0) -> 0
p(s(x)) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Ordered by Num of Vars and Symbs Procedure:
-> Rules:
 +(x,y) -> br(y,x,+(s(x),p(y)))
 +(x,y) -> br(x,y,+(p(x),s(y)))
 br(0,y,z) -> y
 br(s(x),y,z) -> z
 p(0) -> 0
 p(s(x)) -> x
-> Vars:
 y, x, y, x, y, z, y, z, x, x

-> Rlps:
 (rule: +(x,y) -> br(y,x,+(s(x),p(y))), id: 1, possubterms: +(x,y)->[])
 (rule: +(x,y) -> br(x,y,+(p(x),s(y))), id: 2, possubterms: +(x,y)->[])
 (rule: br(0,y,z) -> y, id: 3, possubterms: br(0,y,z)->[], 0->[1])
 (rule: br(s(x),y,z) -> z, id: 4, possubterms: br(s(x),y,z)->[], s(x)->[1])
 (rule: p(0) -> 0, id: 5, possubterms: p(0)->[], 0->[1])
 (rule: p(s(x)) -> x, id: 6, possubterms: p(s(x))->[], s(x)->[1])

-> Unifications:
(R2 unifies with R1 at p: [], l: +(x,y), lp: +(x,y), sig: {y -> y',x -> x'}, l': +(x',y'), r: br(x,y,+(p(x),s(y))), r': br(y',x',+(s(x'),p(y'))))

-> Critical pairs info:
<br(y',x',+(s(x'),p(y'))),br(x',y',+(p(x'),s(y')))>   =>  Not trivial, Overlay, Proper, NW0, N1

-> Problem conclusions:
 Left linear, Not right linear, Not linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR y z x y' x')
(REPLACEMENT-MAP
(+ 1, 2)
(br 1, 2, 3)
(p 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
+(x,y) -> br(y,x,+(s(x),p(y)))
+(x,y) -> br(x,y,+(p(x),s(y)))
br(0,y,z) -> y
br(s(x),y,z) -> z
p(0) -> 0
p(s(x)) -> x
)
Critical Pairs:
<br(y',x',+(s(x'),p(y'))),br(x',y',+(p(x'),s(y')))>   =>  Not trivial, Overlay, Proper, NW0, N1
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

No Convergence InfChecker Procedure:
Infeasible convergence?
YES

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty y z x y1 x1 vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(+ 1 2)
(br 1 2 3)
(p 1)
(0)
(c_x1)
(c_y1)
(fSNonEmpty)
(s 1)
)
(RULES
+(x,y) -> br(y,x,+(s(x),p(y)))
+(x,y) -> br(x,y,+(p(x),s(y)))
br(0,y,z) -> y
br(s(x),y,z) -> z
p(0) -> 0
p(s(x)) -> x
)]
Infeasibility Conditions:
br(c_y1,c_x1,+(s(c_x1),p(c_y1))) ->* z0, br(c_x1,c_y1,+(p(c_x1),s(c_y1))) ->* z0

Problem 1: 

Obtaining a model using AGES:

 -> Theory (Usable Rules):
+(x,y) -> br(y,x,+(s(x),p(y)))
+(x,y) -> br(x,y,+(p(x),s(y)))
br(0,y,z) -> y
br(s(x),y,z) -> z
p(0) -> 0
p(s(x)) -> x

 -> AGES Output:




The problem is infeasible.


The problem is not confluent.