(VAR b d ds v1 v2 v3 v4 x y z )
(RULES 
        T(ok(sys(x,p(d,0),r(0),y))) -> T(check(sys(x,bot,r(1),y)))
        T(ok(sys(x,p(d,1),r(1),y))) -> T(check(sys(x,bot,r(0),y)))
        T(ok(sys(S(0,c(d,ds)),bot,y,z))) ->= T(check(sys(S(0,c(d,ds)),p(d,0),y,z)))
        T(ok(sys(S(1,c(d,ds)),bot,y,z))) ->= T(check(sys(S(0,c(d,ds)),p(d,1),y,z)))
        T(ok(sys(S(0,c(d,ds)),x,y,f(0)))) ->= T(check(sys(S(1,ds),x,y,bot)))
        T(ok(sys(S(1,c(d,ds)),x,y,f(1)))) ->= T(check(sys(S(0,ds),x,y,bot)))
        T(ok(sys(x,y,r(0),bot))) ->= T(check(sys(x,y,r(0),f(1))))
        T(ok(sys(x,y,r(1),bot))) ->= T(check(sys(x,y,r(1),f(0))))
        nils ->= c(new,nils)
        p(d,b) ->= bot
        f(b) ->= bot
        check(old) ->= ok(old)
        check(r(v1)) ->= r(check(v1))
        r(ok(v1)) ->= ok(r(v1))
        check(f(v1)) ->= f(check(v1))
        f(ok(v1)) ->= ok(f(v1))
        check(p(v1,v2)) ->= p(v1,check(v2))
        check(p(v1,v2)) ->= p(check(v1),v2)
        p(v1,ok(v2)) ->= ok(p(v1,v2))
        p(ok(v1),v2) ->= ok(p(v1,v2))
        check(c(v1,v2)) ->= c(v1,check(v2))
        check(c(v1,v2)) ->= c(check(v1),v2)
        c(v1,ok(v2)) ->= ok(c(v1,v2))
        c(ok(v1),v2) ->= ok(c(v1,v2))
        check(S(v1,v2)) ->= S(v1,check(v2))
        check(S(v1,v2)) ->= S(check(v1),v2)
        S(v1,ok(v2)) ->= ok(S(v1,v2))
        S(ok(v1),v2) ->= ok(S(v1,v2))
        check(sys(v1,v2,v3,v4)) ->= sys(v1,v2,v3,check(v4))
        check(sys(v1,v2,v3,v4)) ->= sys(v1,v2,check(v3),v4)
        check(sys(v1,v2,v3,v4)) ->= sys(v1,check(v2),v3,v4)
        check(sys(v1,v2,v3,v4)) ->= sys(check(v1),v2,v3,v4)
        sys(v1,v2,v3,ok(v4)) ->= ok(sys(v1,v2,v3,v4))
        sys(v1,v2,ok(v3),v4) ->= ok(sys(v1,v2,v3,v4))
        sys(v1,ok(v2),v3,v4) ->= ok(sys(v1,v2,v3,v4))
        sys(ok(v1),v2,v3,v4) ->= ok(sys(v1,v2,v3,v4))
)