You cannot nest primes in TLA+ formulas, for good reasons related to stuttering invariance. You want to specify a state machine that monitors the progress of unlocking. Perhaps something along the following lines:
Digit == 0 .. 9
CONSTANT Code \* can be instantiated to <<3,2,1>>, for example
ASSUME Code \in Seq(Digit)
VARIABLES
locked, \* status of the lock
idx \* monitor progression in input of the code
Init ==
/\ locked = TRUE
/\ idx = 1
Input(x) ==
\/ \* user input correct digit
/\ idx <= Len(Code) /\ x = Code[idx]
/\ idx' = idx+1
/\ locked' = (idx < Len(Code)) \* unlock when last digit has been input
\/ \* user input incorrect digit
/\ idx <= Len(Code) /\ x # Code[idx]
/\ idx' = Len(Code)+1 \* make further inputs useless
/\ locked' = locked
\/ \* ignore input when beyond the length of the code
/\ idx > Len(Code)
/\ UNCHANGED <<locked, idx>>
Spec == Init /\ [][\E x \in Digit : Input(x)]_<<locked,idx>>
The last disjunct of the Input action is in fact useless here, since stuttering is always allowed, but it may be useful when interaction with the user is modeled through an explicit interface. Also, you may choose to have a different strategy of handling input errors such as tolerating a certain number of wrong inputs before blocking.
Stephan