While reading the paper Holistic twig joins: optimal XML pattern matching I came across the pseudo code for liststack algorithm. (available through google scholar)

A function in the algorithm confused me, since I can understand what it is supposed to do, but can't deconstruct the notation:

$\qquad \mathtt{Function}\ \mathtt{end}(q\mathtt) \\
 \qquad\qquad \mathtt{return}\ \forall q_i \in \mathtt{subtreeNodes}(q) : \mathtt{isLeaf}(q_i) \implies \mathtt{eof}(T_{q_i})$

This function is supposed to return a single boolean result. It is supposed to be true when all lists associated to leaf nodes of a query pattern node are at their end. So true means there are no more nodes in the query pattern to process.

But what is the meaning of the set builder(ish?) notation here? Is it 

$\qquad$ "for all subtree nodes of $q$ for which $\mathtt{isLeaf}(q_i)$ is true $\mathtt{eof}(T_{q_i})$ is also true"

(which means that the list is at the end position)? 

Or is it 

$\qquad$ "for all subtree nodes of $q$, $\mathtt{isLeaf}(q_i)$ implies $\mathtt{eof}(T_{q_i})$ is true"? 

Is double arrow representing implies with its truth table? 

As you can see, I'm having a bit difficulty in associating the colon and its precedence.

For simplicity, I'll begin by only considering "decision" problems, which have a yes/no answer. Function problems work roughly the same way, except instead of yes/no, there is a specific output word associated with each input word.
Language: a language is simply a set of strings. If you have an alphabet, such as
$\Sigma$, then $\Sigma^*$ is the set of all words containing only the symbols in $\Sigma$.
For example, $\{0,1 \}^*$ is the set of all binary sequences of any length.
An alphabet doesn't need to be binary, though. It can be unary, ternary, etc.
A language over an alphabet $\Sigma$ is any subset of $\Sigma^*$.
Problem: A problem is some question about some input we'd like answered. Specifically, a decision problem is a question which asks, "Does our given input fulfill property $X$?
A language is the formal realization of a problem. When we want to reason theoretically about a decision problem, we often examine the corresponding language.
For a decision problem $X$, the corresponding language is:

$L = \{w \mid w$ is the encoding of an input $y$ to problem $X$,
and the answer to input $y$ for problem $X$ is "Yes"  $ \}$

Determining if the answer for an input to a decision problem is "yes" is equivalent to determining whether an encoding of that input over an alphabet is in the corresponding language.
Algorithm: An algorithm is a step-by-step way to solve a problem. Note that there an algorithm can be expressed in many ways and many languages, and that there are many different algorithms solving any given problem.
Turing Machine: A Turing Machine is the formal analogue of an algorithm. A Turing Machine over a given alphabet, for each word, either will or won't halt in an accepting state. Thus for each Turing Machine $M$, there is a corresponding language:

$L(M) = \{w \mid M$ halts in an accepting state on input $w\}$.

(There's a subtle difference between Turing Machines that halt on all inputs and halt on yes inputs, which defines the difference between complexity classes $\mathsf{R}$ and $\mathsf{RE}$.)
The relationship between languages and Turing Machines is as follows

Every Turing Machine accepts exactly one language

There may be more than one Turing Machine that accept a given language

There may be no Turing Machine that accepts a given language.


We can say roughly the same thing about algorithms and problems: every algorithm solves a single problem, but there may be 0, or many, algorithms solving a given problem.
Time Complexity: One of the most common sources of confusion between algorithms and problems is in regards to complexity classes. The correct allocation can be summarized as follows:

An algorithm has a time complexity
A problem belongs to a complexity class

An algorithm can have a certain time complexity. We say an algorithm has a worst-case upper-bounded complexity
$f(n)$ if the algorithm halts in at most $f(n)$ steps for any input of size $n$.
Problems don't have run-times, since a problem isn't tied to a specific algorithm which actually runs. Instead, we say that a problem belongs to a complexity class, if there exists some algorithm solving that problem with a given time complexity.
$\mathsf{P}, \mathsf{NP}, \mathsf{PSPACE}, \mathsf{EXPTIME}$ etc. are all complexity classes. This means they contain problems, not algorithms. An algorithm can never be in $\mathsf{P}$, but if there's a polynomial-time algorithm solving a given problem $X$, then $X$ can be classified in complexity class $\mathsf{P}$. There could also be a bunch of other algorithms runs in different time complexity will also be able to solve the problem with the same input size under different time complexity, i.e. exponential-time algorithms, but since there already exists a single polynomial-time algorithm accepting $X$, it is in $\mathsf{P}$.
