Hi Ron,
I should point out another problematic part of what you wrote--namely:
<<s, t>>[[(CAPTURE e)']] = 1
The semantics of prime is that
<<s, t>>[[exp']] = t[[exp]].
Therefore, your equality implies that t[[CAPTURE e]] = 1. Why does
t[[x]] = 2 imply that t[[CAPTURE x]] = 1?
Leslie