(VAR b d ds v1 v4 x y z )
(RULES 
        T(ok(sys(x,P(d,b),R(b),y))) -> T(check(sys(x,bot,R(not(b)),y)))
        T(ok(sys(S(b,c(d,ds)),bot,y,z))) ->= T(check(sys(S(b,c(d,ds)),P(d,b),y,z)))
        T(ok(sys(S(b,c(d,ds)),x,y,F(b)))) ->= T(check(sys(S(not(b),ds),x,y,bot)))
        T(ok(sys(x,y,R(b),bot))) ->= T(check(sys(x,y,R(b),F(not(b)))))
        not(1) ->= 0
        not(0) ->= 1
        nils ->= c(new,nils)
        p(d,b) ->= bot
        f(b) ->= bot
        check(old) ->= ok(old)
        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(R(v1)) ->= R(check(v1))
        R(ok(v1)) ->= ok(R(v1))
        check(not(v1)) ->= not(check(v1))
        not(ok(v1)) ->= ok(not(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))
)