Man, fuckin' score one more for formal methods. The proof was starting to get a little difficult, and it led me straight to a bug in the definition. I am still in a good mood, because I remain for the time being under the impression that the fix is easy; I simply failed to do a case analysis in one spot, and erroneously carried out the correct "re-marking" behavior required for one branch in both branches. What I'm supposed to be doing in the other branch is simply not doing the re-marking pass, so that should be easy.
I was skeptical about Alias for the first few episodes, but episodes 5-9 have been pure, brain-fucking gold. I start to get persuaded that maybe some of Steven Johnson's arguments might hold water when shows like this require the viewer to untangle such messes of double-crossings and characters reasoning about other characters' reasoning about them.