YES Problem: 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)) Proof: DP Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) union#(edge(x,y,i),h) -> union#(i,h) reach#(x,y,edge(u,v,i),h) -> eq#(x,u) 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) -> eq#(y,v) 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#(false(),x,y,edge(u,v,i),h) -> union#(i,h) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) 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)) TRS: 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)) EDG Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) union#(edge(x,y,i),h) -> union#(i,h) reach#(x,y,edge(u,v,i),h) -> eq#(x,u) 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) -> eq#(y,v) 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#(false(),x,y,edge(u,v,i),h) -> union#(i,h) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) 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)) TRS: 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)) graph: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) -> reach#(x,y,edge(u,v,i),h) -> eq#(x,u) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) -> reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) -> reach#(x,y,edge(u,v,i),h) -> eq#(x,u) if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) -> reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_2#(false(),x,y,edge(u,v,i),h) -> union#(i,h) -> union#(edge(x,y,i),h) -> union#(i,h) if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) -> reach#(x,y,edge(u,v,i),h) -> eq#(x,u) if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) -> 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#(false(),x,y,edge(u,v,i),h) -> union#(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#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) 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#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,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#(false(),x,y,edge(u,v,i),h) -> or#(reach(x,y,i,h),reach(v,y,union(i,h),empty())) if_reach_1#(true(),x,y,edge(u,v,i),h) -> eq#(y,v) -> eq#(s(x),s(y)) -> eq#(x,y) 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) -> eq#(y,v) 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) reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) -> if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,h)) reach#(x,y,edge(u,v,i),h) -> eq#(x,u) -> eq#(s(x),s(y)) -> eq#(x,y) union#(edge(x,y,i),h) -> union#(i,h) -> union#(edge(x,y,i),h) -> union#(i,h) eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) SCC Processor: #sccs: 3 #rules: 7 #arcs: 18/121 DPs: if_reach_2#(false(),x,y,edge(u,v,i),h) -> reach#(v,y,union(i,h),empty()) reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,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#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,h) TRS: 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [if_reach_2#](x0, x1, x2, x3, x4) = x3 + x4, [if_reach_1#](x0, x1, x2, x3, x4) = x3 + x4, [reach#](x0, x1, x2, x3) = x2 + x3, [if_reach_2](x0, x1, x2, x3, x4) = 0, [if_reach_1](x0, x1, x2, x3, x4) = 0, [reach](x0, x1, x2, x3) = 0, [edge](x0, x1, x2) = x0 + x2 + 1, [union](x0, x1) = x0 + x1, [empty] = 0, [or](x0, x1) = x1, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: if_reach_2#(false(),x,y,edge(u,v,i),h) = h + i + u + 1 >= h + i = reach#(v,y,union(i,h),empty()) reach#(x,y,edge(u,v,i),h) = h + i + u + 1 >= h + i + u + 1 = if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_1#(false(),x,y,edge(u,v,i),h) = h + i + u + 1 >= h + i + u + 1 = reach#(x,y,i,edge(u,v,h)) if_reach_1#(true(),x,y,edge(u,v,i),h) = h + i + u + 1 >= h + i + u + 1 = if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) if_reach_2#(false(),x,y,edge(u,v,i),h) = h + i + u + 1 >= h + i = reach#(x,y,i,h) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(x)) = 0 >= 0 = false() eq(s(x),0()) = 0 >= 0 = false() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) or(true(),y) = y >= 0 = true() or(false(),y) = y >= y = y union(empty(),h) = h >= h = h union(edge(x,y,i),h) = h + i + x + 1 >= h + i + x + 1 = edge(x,y,union(i,h)) reach(x,y,empty(),h) = 0 >= 0 = false() reach(x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_1(eq(x,u),x,y,edge(u,v,i),h) if_reach_1(true(),x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_2(eq(y,v),x,y,edge(u,v,i),h) if_reach_2(true(),x,y,edge(u,v,i),h) = 0 >= 0 = true() if_reach_2(false(),x,y,edge(u,v,i),h) = 0 >= 0 = or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) if_reach_1(false(),x,y,edge(u,v,i),h) = 0 >= 0 = reach(x,y,i,edge(u,v,h)) problem: DPs: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_1#(false(),x,y,edge(u,v,i),h) -> reach#(x,y,i,edge(u,v,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) TRS: 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)) Subterm Criterion Processor: simple projection: pi(reach#) = 2 pi(if_reach_1#) = 3 pi(if_reach_2#) = 3 problem: DPs: 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) TRS: 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [if_reach_2#](x0, x1, x2, x3, x4) = 0, [if_reach_1#](x0, x1, x2, x3, x4) = 1, [reach#](x0, x1, x2, x3) = 1, [if_reach_2](x0, x1, x2, x3, x4) = 0, [if_reach_1](x0, x1, x2, x3, x4) = 0, [reach](x0, x1, x2, x3) = 0, [edge](x0, x1, x2) = x2, [union](x0, x1) = x1, [empty] = 0, [or](x0, x1) = x1, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: reach#(x,y,edge(u,v,i),h) = 1 >= 1 = if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) if_reach_1#(true(),x,y,edge(u,v,i),h) = 1 >= 0 = if_reach_2#(eq(y,v),x,y,edge(u,v,i),h) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(x)) = 0 >= 0 = false() eq(s(x),0()) = 0 >= 0 = false() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) or(true(),y) = y >= 0 = true() or(false(),y) = y >= y = y union(empty(),h) = h >= h = h union(edge(x,y,i),h) = h >= h = edge(x,y,union(i,h)) reach(x,y,empty(),h) = 0 >= 0 = false() reach(x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_1(eq(x,u),x,y,edge(u,v,i),h) if_reach_1(true(),x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_2(eq(y,v),x,y,edge(u,v,i),h) if_reach_2(true(),x,y,edge(u,v,i),h) = 0 >= 0 = true() if_reach_2(false(),x,y,edge(u,v,i),h) = 0 >= 0 = or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) if_reach_1(false(),x,y,edge(u,v,i),h) = 0 >= 0 = reach(x,y,i,edge(u,v,h)) problem: DPs: reach#(x,y,edge(u,v,i),h) -> if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) TRS: 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)) Matrix Interpretation Processor: dimension: 1 interpretation: [if_reach_1#](x0, x1, x2, x3, x4) = 0, [reach#](x0, x1, x2, x3) = 1, [if_reach_2](x0, x1, x2, x3, x4) = 0, [if_reach_1](x0, x1, x2, x3, x4) = 0, [reach](x0, x1, x2, x3) = 0, [edge](x0, x1, x2) = x2, [union](x0, x1) = x1, [empty] = 0, [or](x0, x1) = x1, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: reach#(x,y,edge(u,v,i),h) = 1 >= 0 = if_reach_1#(eq(x,u),x,y,edge(u,v,i),h) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(x)) = 0 >= 0 = false() eq(s(x),0()) = 0 >= 0 = false() eq(s(x),s(y)) = 0 >= 0 = eq(x,y) or(true(),y) = y >= 0 = true() or(false(),y) = y >= y = y union(empty(),h) = h >= h = h union(edge(x,y,i),h) = h >= h = edge(x,y,union(i,h)) reach(x,y,empty(),h) = 0 >= 0 = false() reach(x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_1(eq(x,u),x,y,edge(u,v,i),h) if_reach_1(true(),x,y,edge(u,v,i),h) = 0 >= 0 = if_reach_2(eq(y,v),x,y,edge(u,v,i),h) if_reach_2(true(),x,y,edge(u,v,i),h) = 0 >= 0 = true() if_reach_2(false(),x,y,edge(u,v,i),h) = 0 >= 0 = or(reach(x,y,i,h),reach(v,y,union(i,h),empty())) if_reach_1(false(),x,y,edge(u,v,i),h) = 0 >= 0 = reach(x,y,i,edge(u,v,h)) problem: DPs: TRS: 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)) Qed DPs: union#(edge(x,y,i),h) -> union#(i,h) TRS: 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)) Subterm Criterion Processor: simple projection: pi(union#) = 0 problem: DPs: TRS: 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)) Qed DPs: eq#(s(x),s(y)) -> eq#(x,y) TRS: 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)) Subterm Criterion Processor: simple projection: pi(eq#) = 1 problem: DPs: TRS: 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)) Qed