Variable substitution error in Pi-calculus

Question

I am learning the language K, so I started a little implementation of the Pi-Calculus with K. I can't figure out why my substitution Q[Z/Y] doesn't work in my program below.

My program is: (m(z) . m ! z) | (m ! 4 . m(x)) (a ping/pong between two thread), and with my K semantic below I get this output:

</thread> <thread>
    <k>
      m ! z ~> .
    </k>
  </thread> <thread>
    <k>
      m ( x ) ~> .
    </k>

But z is not substituted. I would expect this output:

</thread> <thread>
    <k>
      m ! 4 ~> .      <---The 2nd z take the value of 4
    </k>
  </thread> <thread>
    <k>
      m ( x ) ~> .
    </k>

Here is my K semantic for the Pi-calculus. Notice that I use x!y instead of x<y> for the send construction.

require "substitution.md"

module PI-SYNTAX 
    imports DOMAINS-SYNTAX
    imports KVAR-SYNTAX

    syntax Val ::= KVar  [binder]
                | Int

    syntax Proc ::= "(" Proc ")"        [bracket]
                | Send
                | Receive
                | None
                | Replication
                > Proc "." Proc         [left]
                > Par

    syntax None ::= "None"

    syntax Par ::= Proc "|" Proc        [left]

    syntax Receive ::= Id "(" Val ")"   

    syntax Send ::= Id "!" Val

    syntax Replication ::= "!" Proc

endmodule

module PI
    imports PI-SYNTAX
    imports DOMAINS
    imports SUBSTITUTION

    syntax KResult ::= Int | Bool

      configuration <T color="yellow">
                        <thread multiplicity="*" type="Set" color="blue">
                            <k color="green"> $PGM:Proc </k>
                        </thread>
                    </T>

    // Parallel composition:
    rule <thread> <k> P1:Proc | P2:Proc => . ... </k> </thread>
        (.Bag => <thread> <k> P1 </k> </thread>)
        (.Bag => <thread> <k> P2 </k> </thread>)

    // Communicate reduction: x ! y . P | x(y) . Q => P | Q[z/y]
    rule
        <thread> ... <k> X:Id ! Y:Val . P:Proc => P </k> ... </thread>
        <thread> ... <k> X:Id ( Z:Val ) . Q:Proc => Q[Z/Y] </k> ... </thread>
endmodule

Thank you in advance.