A general way of expressing properties that are not obviously expressible using just  and <> is to specify a state machine expressing the property, then prove that the algorithm implements that state machine. For your example you could write a module along the following lines.
------ MODULE ProcQueue ------
EXTENDS Naturals, Sequences
Init == q = <<>>
/\ ~ \E i \in 1 .. Len(q) : q[i] = self
/\ q’ = Append(q, self)
/\ q # <<>>
/\ Head(q) = self
/\ q’ = Tail(q)
Spec == Init /\ [\E self \in ProcSet : Req(self) \/ Grant(self)]_q
In the module that contains the specification of your filter algorithm, you then add
FCFS == INSTANCE ProcQueue WITH q <- …
and ask TLC to check the property FCFS!Spec.
The potentially tricky part is to define the substitution for q that computes the queue of waiting processes from the state of the filter algorithm (this is usually called a “refinement mapping”). The idea is that the queue contains the processes that are “in_filter” but not yet “in_cs”. The Req action of ProcQueue corresponds to a process transition from not_in_filter to in_filter in the implementation (or perhaps the first step in case this requires a sequence of transitions), and the Grant action corresponds to the transition leading to process state cs. Since the high-level state machine is explicitly based on a queue, it is obvious that it ensures an FCFS policy.