Because signatures in method specifications of an interface may refer to the interface itself,
there may be cyclic dependencies that then result in well-foundness issues of the definition of logical relations.
To solve this issue we include a step index [1]}.
We explain this technical point via the example in Figure REF .
We will write \( e \approx E \in \llbracket t\rrbracket _{k} \)  to denote that FG expression \(e\)  and TL expression \(E\) 
are in a logical relation w.r.t. the FG type \(t\) , where \(k\)  is the step index.
Similarly, \( \mbox{\normalfont \bfseries \sffamily func}\ (x \ t_S) \ R \ \lbrace  \mbox{\normalfont \bfseries \sffamily return}\ e \rbrace  \approx V \in \llbracket R\rrbracket _{k} \)  expresses
that a FG method declaration and a TL value \(V\)  are in a logical relation w.r.t. the FG method
specification \(R\) .
