Text this: Proving acceptability properties of relaxed nondeterministic approximate programs