(VAR x y z )
(RULES 
        top(ok(left(car(x,y),z))) -> top(check(right(y,z)))
        top(ok(right(x,car(y,z)))) -> top(check(left(x,z)))
        top(ok(left(bot,x))) -> top(check(right(bot,x)))
        top(ok(right(x,bot))) -> top(check(left(x,bot)))
        top(ok(left(car(x,y),z))) ->= top(check(left(y,z)))
        top(ok(right(x,car(y,z)))) ->= top(check(right(x,z)))
        bot ->= car(new,bot)
        check(old) ->= ok(old)
        check(car(x,y)) ->= car(check(x),y)
        check(car(x,y)) ->= car(x,check(y))
        check(left(x,y)) ->= left(check(x),y)
        check(left(x,y)) ->= left(x,check(y))
        check(right(x,y)) ->= right(check(x),y)
        check(right(x,y)) ->= right(x,check(y))
        car(ok(x),y) ->= ok(car(x,y))
        car(x,ok(y)) ->= ok(car(x,y))
        left(ok(x),y) ->= ok(left(x,y))
        left(x,ok(y)) ->= ok(left(x,y))
        right(ok(x),y) ->= ok(right(x,y))
        right(x,ok(y)) ->= ok(right(x,y))
)