Braces are substitution, so

  b{a/x}

means: expression b with variable x inside it replaced by expression a. So their beta-reduction line just says that if

  k = ... (λx.b) a ...

it can be reduced to

  k = ... c ...

where c is the expression b, but with all occurrences of variable x replaced by expression a.

I think Tk(x) denotes "the definition of variable k is expression x" and the square brackets are "k[x]" something like "in the context of definition k, value of expression x". So I suspect that

  a=Tk(x)
  a[y]

would be effectively

  (λk.y)x

But yes, not very clear on explaining the notation. Also seems to have some typos e.g. at the beginning have "x ∈ k, x, y" which looks to me should be "x ∋ k, x, y" (or of course "k, x, y ∈ x").

yeah no idea