\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\[\axjustifies\trans{\StmPush~\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\StmPush~\texttt{"u"}:\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$s$"}:\texttt{"$t$"}:\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rule{assumption}{}}\]
\justifies{}\trans{\StmPush~\texttt{"c$s$"}:\StmPush~\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\StmPush~\texttt{"u"}:\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"$t$"}:\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPush~\texttt{"$t$"}:\StmPush~\texttt{"c$s$"}:\StmPush~\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\StmPush~\texttt{"u"}:\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\Nil,\{\texttt{""}\mapsto\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"},\texttt{"\textit{tl}(c$t$)"}\mapsto\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"},\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rexecns}\]
\justifies{}\trans{\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{""}\mapsto\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"},\texttt{"\textit{tl}(c$t$)"}\mapsto\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"},\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{""}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"\textit{tl}(c$t$)"}\mapsto\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"},\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"\textit{tl}(c$t$)"}\mapsto\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"},\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textit{tl}(c$t$)"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rcatns}\]
\justifies{}\trans{\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"u"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rcatns}\]
\justifies{}\trans{\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gh\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gt\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}p\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}g\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}o\textbackslash{}\textquotedblright{}+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}v\textbackslash{}\textquotedblright{}gq\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}gq++\textbackslash{}\textquotedblright{}u\textbackslash{}\textquotedblright{}g+\textbackslash{}\textquotedblright{}w\textbackslash{}\textquotedblright{}gp\textbackslash{}\textquotedblright{}\textbackslash{}\textquotedblright{}pgx\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rcatns}\]
\justifies{}\trans{\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rquotifyns}\]
\justifies{}\trans{\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"u"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$s$"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rquotifyns}\]
\justifies{}\trans{\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"v"}:\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}\textit{tl}(c\textit{q}($t$))\textquotedblright{}"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textit{tl}(c$t$)"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rquotifyns}\]
\justifies{}\trans{\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}o"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"o"}:\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rcatns}\]
\justifies{}\trans{\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}c\textit{q}($s$)\textquotedblright{}"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$s$"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rquotifyns}\]
\justifies{}\trans{\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"v"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\Nil,\{\texttt{"w"}\mapsto\texttt{"\textit{tl}(c$t$)"},\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textit{tl}(c$t$)"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$t$"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rtailns}\]
\justifies{}\trans{\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\Nil,\{\texttt{"v"}\mapsto\texttt{"c$s$"},\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"v"}:\texttt{"c$s$"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$s$"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"$s$"}:\texttt{"c"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rcatns}\]
\justifies{}\trans{\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"v"}:\texttt{"c"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$t$"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rheadns}\]
\justifies{}\trans{\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rgetns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\Nil,\{\texttt{"w"}\mapsto\texttt{"c$t$"},\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"w"}:\texttt{"c$t$"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"c$t$"}:\Nil,\{\texttt{"v"}\mapsto\texttt{"$s$"},\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"v"}:\texttt{"$s$"}:\texttt{"c$t$"}:\Nil,\{\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"$s$"}:\texttt{"c$t$"}:\Nil,\{\texttt{"u"}\mapsto\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}\}\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"u"}:\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"$s$"}:\texttt{"c$t$"}:\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rputns}\]
\justifies{}\trans{\StmPush~\texttt{"u"}:\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\texttt{"$s$"}:\texttt{"c$t$"}:\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}\]
\justifies{}\trans{\StmPush~\texttt{"\textquotedblright{}u\textquotedblright{}p\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gh\textquotedblright{}v\textquotedblright{}g+\textquotedblright{}v\textquotedblright{}p\textquotedblright{}w\textquotedblright{}gt\textquotedblright{}w\textquotedblright{}p\textquotedblright{}w\textquotedblright{}g\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}o\textquotedblright{}+\textquotedblright{}w\textquotedblright{}gq\textquotedblright{}v\textquotedblright{}gq\textquotedblright{}u\textquotedblright{}gq++\textquotedblright{}u\textquotedblright{}g+\textquotedblright{}w\textquotedblright{}gp\textquotedblright{}\textquotedblright{}pgx"}:\StmPush~\texttt{"u"}:\StmPut:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmHead:\StmPush~\texttt{"v"}:\StmGet:\StmCat:\StmPush~\texttt{"v"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmTail:\StmPush~\texttt{"w"}:\StmPut:\StmPush~\texttt{"w"}:\StmGet:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"o"}:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmQuotify:\StmPush~\texttt{"v"}:\StmGet:\StmQuotify:\StmPush~\texttt{"u"}:\StmGet:\StmQuotify:\StmCat:\StmCat:\StmPush~\texttt{"u"}:\StmGet:\StmCat:\StmPush~\texttt{"w"}:\StmGet:\StmPut:\StmPush~\texttt{""}:\StmPut:\StmGet:\StmExec}{\Nil}{\left(\texttt{"$s$"}:\texttt{"c$t$"}:\Nil,\emptyset\right)}{\Nil}{\texttt{"$t^R$c$s$"}:\Nil}{\left(\Nil,\emptyset\right)}\using{\rpushns}