and(and(all(r, v), implies(u, not(not(u)))), not(and(all(r, v), implies(u, not(not(u)))))