- [ inl s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
- 〈inr … (inl … news2),m〉
- | inr s3 ⇒ let 〈news3,m〉 ≝ trans sig M3 〈s3,a〉 in
- 〈inr … (inr … news3),m〉
+ [ inl s2 ⇒ let 〈news2,newa,m〉 ≝ trans sig M2 〈s2,a〉 in
+ 〈inr … (inl … news2),newa,m〉
+ | inr s3 ⇒ let 〈news3,newa,m〉 ≝ trans sig M3 〈s3,a〉 in
+ 〈inr … (inr … news3),newa,m〉