Input TRS:
    1: T(ok(sys(x,p(d,0()),r(0()),y))) -> T(check(sys(x,bot(),r(1()),y)))
    2: T(ok(sys(x,p(d,1()),r(1()),y))) -> T(check(sys(x,bot(),r(0()),y)))
   e1: T(ok(sys(S(0(),c(d,ds)),bot(),y,z))) ->= T(check(sys(S(0(),c(d,ds)),p(d,0()),y,z)))	[relative]
   e2: T(ok(sys(S(1(),c(d,ds)),bot(),y,z))) ->= T(check(sys(S(0(),c(d,ds)),p(d,1()),y,z)))	[relative]
   e3: T(ok(sys(S(0(),c(d,ds)),x,y,f(0())))) ->= T(check(sys(S(1(),ds),x,y,bot())))	[relative]
   e4: T(ok(sys(S(1(),c(d,ds)),x,y,f(1())))) ->= T(check(sys(S(0(),ds),x,y,bot())))	[relative]
   e5: T(ok(sys(x,y,r(0()),bot()))) ->= T(check(sys(x,y,r(0()),f(1()))))	[relative]
   e6: T(ok(sys(x,y,r(1()),bot()))) ->= T(check(sys(x,y,r(1()),f(0()))))	[relative]
   e7: nils() ->= c(new(),nils())	[relative]
   e8: p(d,b) ->= bot()	[relative]
   e9: f(b) ->= bot()	[relative]
   e10: check(old()) ->= ok(old())	[relative]
   e11: check(r(v1)) ->= r(check(v1))	[relative]
   e12: r(ok(v1)) ->= ok(r(v1))	[relative]
   e13: check(f(v1)) ->= f(check(v1))	[relative]
   e14: f(ok(v1)) ->= ok(f(v1))	[relative]
   e15: check(p(v1,v2)) ->= p(v1,check(v2))	[relative]
   e16: check(p(v1,v2)) ->= p(check(v1),v2)	[relative]
   e17: p(v1,ok(v2)) ->= ok(p(v1,v2))	[relative]
   e18: p(ok(v1),v2) ->= ok(p(v1,v2))	[relative]
   e19: check(c(v1,v2)) ->= c(v1,check(v2))	[relative]
   e20: check(c(v1,v2)) ->= c(check(v1),v2)	[relative]
   e21: c(v1,ok(v2)) ->= ok(c(v1,v2))	[relative]
   e22: c(ok(v1),v2) ->= ok(c(v1,v2))	[relative]
   e23: check(S(v1,v2)) ->= S(v1,check(v2))	[relative]
   e24: check(S(v1,v2)) ->= S(check(v1),v2)	[relative]
   e25: S(v1,ok(v2)) ->= ok(S(v1,v2))	[relative]
   e26: S(ok(v1),v2) ->= ok(S(v1,v2))	[relative]
   e27: check(sys(v1,v2,v3,v4)) ->= sys(v1,v2,v3,check(v4))	[relative]
   e28: check(sys(v1,v2,v3,v4)) ->= sys(v1,v2,check(v3),v4)	[relative]
   e29: check(sys(v1,v2,v3,v4)) ->= sys(v1,check(v2),v3,v4)	[relative]
   e30: check(sys(v1,v2,v3,v4)) ->= sys(check(v1),v2,v3,v4)	[relative]
   e31: sys(v1,v2,v3,ok(v4)) ->= ok(sys(v1,v2,v3,v4))	[relative]
   e32: sys(v1,v2,ok(v3),v4) ->= ok(sys(v1,v2,v3,v4))	[relative]
   e33: sys(v1,ok(v2),v3,v4) ->= ok(sys(v1,v2,v3,v4))	[relative]
   e34: sys(ok(v1),v2,v3,v4) ->= ok(sys(v1,v2,v3,v4))	[relative]
Weak rule e2 is duplicating