/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#3.13.trs

The program

(from AG01 3.13)
(VAR h i u v x y)
(RULES
eq(0,0) -> true
eq(0,s(x)) -> false
eq(s(x),0) -> false
eq(s(x),s(y)) -> eq(x,y)
or(true,y) -> true
or(false,y) -> y
union(empty,h) -> h
union(edge(x,y,i),h) -> edge(x,y,union(i,h))
reach(x,y,empty,h) -> false
reach(x,y,edge(u,v,i),h) -> if_reach_1(eq(x,u),x,y,edge(u,v,i),h)
if_reach_1(true,x,y,edge(u,v,i),h) -> if_reach_2(eq(y,v),x,y,edge(u,v,i),h)
if_reach_2(true,x,y,edge(u,v,i),h) -> true
if_reach_2(false,x,y,edge(u,v,i),h) -> or(reach(x,y,i,h),reach(v,y,union(i,h),empty))
if_reach_1(false,x,y,edge(u,v,i),h) -> reach(x,y,i,edge(u,v,h)))

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend