for S being non empty set
for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f being Assign of (Inf_seqModel (S,BASSIGN)) holds
( t |= 'X' f iff Shift (t,1) |= f )