The part I’m confused about is why Bob converts
Also, I think a weak part of this idea in either conception is that you have to provide a proof to make these exchanges. I think it would be neat for an exchange to have a proof-verifier, but that doesn’t really seem to hold up to the promise of Alice and Bob working collectively to prove
Perhaps another way to go about this is to introduce GL modal logic. Instead of creating shares in and , create shares in and . It’s not possible to exchange a pair of shares in and for cash, because is not a logical tautology.