Second, the only objects which are actually referenced or modified in an instruction are those which the caller is permitted to access; that is, those which are appropriately recorded in the protection data. Otherwise, the instruction must terminate with no effect on any protected object. . . S3) Specific access to protected objects is permitted only when the recorded protection data allows it. . . With these three predicates, we have covered all data security cases: No state transition may reference or modify an object unless a) that object is explicitly named by the instruction, and b) the action is expressly permitted as indicated by recorded protection data. While the three predicates are concerned with single transitions and not sequences of transitions, it is trivially shown by induction that if the predicates are true for all single transitions, they are true for all finite sequences.