Input TRS: 1: topB(i,N1(),y) -> topA(1(),T1(),y) 2: topA(i,x,N2()) -> topB(0(),x,T2()) 3: topB(i,S1(),y) -> topA(i,N1(),y) 4: topA(i,x,S2()) -> topB(i,x,N2()) 5: topA(i,N1(),T2()) -> topB(i,N1(),S2()) 6: topA(1(),T1(),T2()) -> topB(1(),T1(),S2()) e1: topA(i,N1(),y) ->= topA(1(),T1(),y) [relative] e2: topB(i,x,N2()) ->= topB(0(),x,T2()) [relative] e3: topA(i,S1(),y) ->= topA(i,N1(),y) [relative] e4: topB(i,x,S2()) ->= topB(i,x,N2()) [relative] e5: topB(i,N1(),T2()) ->= topB(i,N1(),S2()) [relative] e6: topB(1(),T1(),T2()) ->= topB(1(),T1(),S2()) [relative] Weak rule e6 calls a strict rule