This cannot be implemented in the script today due to disabled op_codes.  Even if it could be, the resulting transactions for the proof of payment redemption would be prohibitively large: They'd have to contain a SPV fragment for the mixer->b,c transaction plus some block headers, and the complete mixer->b,c transaction, and the script search for the right outputs and then check the fragments.

We could perhaps enable this with a soft-forking addition to add an opcode that verifies a SPV fragment, and constrain your protocol that Alice must know the exact transaction the mixer intends to make... e.g. under 400 bytes of data. Very interesting. I'd want to see other use cases for this.

(As an aside, your notation of "from address", "to address" suggest a pretty substantial misunderstanding of the Bitcoin system, likely inspired by block explorer sites that present things in terms of "address = account", this isn't how the protocol actually works.. but what you're describing could be restated in terms that do make sense in the Bitcoin protocol)

If script is ever extended to allow compact proofs of computation then what you're describing could work without huge transactions.  If the proof of computation is zero-knowledge then your protocol could be simplified further: instead of Alice releasing the coins in the faithful execution case the your second party could redeem them using a zero-knowledge proof that Alice's rules were followed, without actually revealing what those rules were.