• 〈 v = e, φα 〉 → 〈 ε, φ[ α.v : = eφ ] 〉

  


  



slide: Transition system -- rules