[6]((),S xs [1.5mu 1.5mu])[E]

[3]run_State (h_State^' pop_S) (S xs (q:stack))=run_State (h_State^' q) (S xs stack)[E]

[6]run_State (h_State^' pop_S) (S xs (q:stack))[E]

[6]run_State (h_State^' (get>>=λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op)) (S xs (q:stack))[E]

[6]run_State (h_State^' (Op (Get η)>>=λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op)) (S xs (q:stack))[E]

[6]run_State (h_State^' (Op (Get (λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op)))) (S xs (q:stack))[E]

[6]run_State (State (λs→run_State (h_State^' ((λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op) s)) s)) (S xs (q:stack))[E]

[6](λs→run_State (h_State^' ((λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op) s)) s) (S xs (q:stack))[E]

[6]run_State (h_State^' ((λ(S xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (S xs ps);op) (S xs (q:stack)))) (S xs (q:stack))[E]

[6]run_State (h_State^' (put (S xs stack)>>q)) (S xs (q:stack))[E]

[6]run_State (h_State^' (Op (Put (S xs stack) (η ()))>>q)) (S xs (q:stack))[E]

[6]run_State (h_State^' (Op (Put (S xs stack) q))) (S xs (q:stack))[E]

[6]run_State (State (λs→run_State (h_State^' q) (S xs stack))) (S xs (q:stack))[E]

[6](λs→run_State (h_State^' q) (S xs stack)) (S xs (q:stack))[E]

[6]run_State (h_State^' q) (S xs stack)[E]

[3]run_State (h_State^' (push_S q p)) (S xs stack)=run_State (h_State^' p) (S xs (q:stack))[E]

[6]run_State (h_State^' (push_S q p)) (S xs stack)[E]

[6]run_State (h_State^' (get>>=λ(S xs stack)→put (S xs (q:stack))>>p)) (S xs stack)[E]

[6]run_State (h_State^' (Op (Get η)>>=λ(S xs stack)→put (S xs (q:stack))>>p)) (S xs stack)[E]

[6]run_State (h_State^' (Op (Get (λ(S xs stack)→put (S xs (q:stack))>>p)))) (S xs stack)[E]

[6]run_State (State (λs→run_State (h_State^' ((λ(S xs stack)→put (S xs (q:stack))>>p) s)) s)) [E]

[8](S xs stack)[E]

[6](λs→run_State (h_State^' ((λ(S xs stack)→put (S xs (q:stack))>>p) s)) s) (S xs stack)[E]

[6]run_State (h_State^' ((λ(S xs stack)→put (S xs (q:stack))>>p) (S xs stack))) (S xs stack)[E]

[6]run_State (h_State^' (put (S xs (q:stack))>>p)) (S xs stack)[E]

[6]run_State (h_State^' (Op (Put (S xs (q:stack)) (η ()))>>p)) (S xs stack)[E]

[6]run_State (h_State^' (Op (Put (S xs (q:stack)) p))) (S xs stack)[E]

[6]run_State (State (λs→run_State (h_State^' p) (S xs (q:stack)))) (S xs stack)[E]

[6](λs→run_State (h_State^' p) (S xs (q:stack))) (S xs stack)[E]

[6]run_State (h_State^' p) (S xs (q:stack))[E]

§.§ Combining with Other Effects

This section proves the following theorem in <Ref>.

The proof is very similar to that of <Ref> in

We start with expanding the definition of :B@>l<@
We use the fold fusion law fusion-post' (<ref>) to
fuse the left-hand side.
Since the right-hand side is already a fold, to prove the equation we
just need to check the components of the fold  satisfy the
conditions of the fold fusion. The conditions can be splitted into
the following three equations:

\[\ba{rl}
&\ensuremath{(\Varid{extract_{SS}}\hsdot{\circ }{.}\Varid{h_{State}})\hsdot{\circ }{.}\Varid{gen}\mathrel{=}\Varid{gen_{ND+f}}} \\
&\ensuremath{(\Varid{extract_{SS}}\hsdot{\circ }{.}\Varid{h_{State}})\hsdot{\circ }{.}\Varid{alg}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{nondet2state_S}}\\
\ensuremath{\mathrel{=}}&  \ensuremath{\Varid{alg_{ND+f}}\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{extract_{SS}}\hsdot{\circ }{.}\Varid{h_{State}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{nondet2state_S}} \\
&\ensuremath{(\Varid{extract_{SS}}\hsdot{\circ }{.}\Varid{h_{State}})\hsdot{\circ }{.}\Varid{fwd}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{nondet2state_S}}\\
\ensuremath{\mathrel{=}}&  \ensuremath{\Varid{fwd_{ND+f}}\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{extract_{SS}}\hsdot{\circ }{.}\Varid{h_{State}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{nondet2state_S}}
\ea\]

For brevity, we omit the last common part  of
the second equation in the following proof. Instead, we assume that
the input is in the codomain of .

For the first equation, we calculate as follows:
[6]extract_SS (h_State (gen x))[E]

[6]extract_SS (h_State (append_SS x pop_SS))[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State (append_SS x pop_SS)) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State pop_SS) (SS ([1.5mu 1.5mu]++[1.5mu x1.5mu]) [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State pop_SS) (SS [1.5mu x1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩η ((),SS [1.5mu x1.5mu] [1.5mu 1.5mu])[E]

[6]η [1.5mu x1.5mu][E]

[6]Var [1.5mu x1.5mu][E]

[6](Var∘.η) x[E]

[6]gen_ND+f x[E]

For the second equation, we proceed with a case analysis on the input.

[6]extract_SS (h_State (alg Fail))[E]

[6]extract_SS (h_State pop_SS)[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State pop_SS) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩η ((),SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]η [1.5mu 1.5mu][E]

[6]Var [1.5mu 1.5mu][E]

[6]alg_ND+f Fail[E]

[6](alg_ND+f∘.fmap (extract_SS∘.h_State)) Fail[E]

[6]extract_SS (h_State (alg (Or p q)))[E]

[6]extract_SS (h_State (push_SS q p))[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State (push_SS q p)) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State p) (SS [1.5mu 1.5mu] [1.5mu q1.5mu])[E]

[8]𝐝𝐨 {1.5mu p'←extract_SS (h_State p);run_StateT (h_State pop_SS) (SS ([1.5mu 1.5mu]++p') [1.5mu q1.5mu])1.5mu}[E]

[6]results_SS∘.snd⟨0.1pt1$⟩𝐝𝐨 {1.5mu p'←extract_SS (h_State p);run_StateT (h_State pop_SS) (SS p' [1.5mu q1.5mu])1.5mu}[E]

[6]results_SS∘.snd⟨0.1pt1$⟩𝐝𝐨 {1.5mu p'←extract_SS (h_State p);run_StateT (h_State q) (SS p' [1.5mu 1.5mu])1.5mu}[E]

[6]results_SS∘.snd⟨0.1pt1$⟩𝐝𝐨 {1.5mu p'←extract_SS (h_State p);[E]

[8]𝐝𝐨 {1.5mu q'←extract_SS (h_State q);run_StateT (h_State pop_SS) (SS (p'++q') [1.5mu 1.5mu])1.5mu}1.5mu}[E]

[6]results_SS∘.snd⟨0.1pt1$⟩𝐝𝐨 {1.5mu p'←extract_SS (h_State p);q'←extract_SS (h_State q);[E]

[8]run_StateT (h_State pop_SS) (SS (p'++q') [1.5mu 1.5mu])1.5mu}[E]

[8]𝐝𝐨 {1.5mu p'←extract_SS (h_State p);q'←extract_SS (h_State q);η ((),SS (p'++q') [1.5mu 1.5mu])1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State p);q'←extract_SS (h_State q);η (p'++q')1.5mu}[E]

[6]liftM2 (++) ((extract_SS∘.h_State) p) ((extract_SS∘.h_State) q)[E]

[6]alg_ND+f (Or ((extract_SS∘.h_State) p) ((extract_SS∘.h_State) q))[E]

[6](alg_ND+f∘.fmap (extract_SS∘.h_State)) (Or p q)[E]

For the last equation, we calculate as follows:

[6]extract_SS (h_State (fwd y))[E]

[6]extract_SS (h_State (Op (Inr y)))[E]

[6]extract_SS (StateT$λs→Op$fmap (λk→run_StateT k s) (fmap h_State y))[E]

[8]run_StateT (StateT$λs→Op$fmap (λk→run_StateT k s) (fmap h_State y)) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩(λs→Op$fmap (λk→run_StateT k s) (fmap h_State y)) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]results_SS∘.snd⟨0.1pt1$⟩Op$fmap (λk→run_StateT k (SS [1.5mu 1.5mu] [1.5mu 1.5mu])) (fmap h_State y))[E]

[6]Op (fmap (λk→results_SS∘.snd⟨0.1pt1$⟩run_StateT k (SS [1.5mu 1.5mu] [1.5mu 1.5mu])) (fmap h_State y))[E]

[6]fwd_ND+f (fmap (λk→results_SS∘.snd⟨0.1pt1$⟩run_StateT k (SS [1.5mu 1.5mu] [1.5mu 1.5mu])) (fmap h_State y))[E]

[6]fwd_ND+f (fmap extract_SS (fmap h_State y))[E]

[6]fwd_ND+f (fmap (extract_SS∘.h_State) y)[E]

In the above proof we have used several lemmas. Now we prove them.

[6]run_StateT (h_State p) (SS xs stack)[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State p);run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]
holds for all  in the codomain of the function .

The proof structure is similar to that of <Ref>.
We prove this lemma by structural induction on .
For each inductive case of , we not only assume this lemma holds
for its sub-terms (this is the standard induction hypothesis), but
also assume <Ref> holds for  and its sub-terms.
This is sound because in the proof of <Ref>, for
, we only apply
<Ref> to the sub-terms of , which is already
included in the induction hypothesis so there is no circular argument.

Since we assume <Ref> holds for  and its
sub-terms, we can use several useful properties proved in the
sub-cases of the proof of <Ref>. We list them here
for easy reference:

* extract-gen-ext:

* extract-alg1-ext:

* extract-alg2-ext:

* extract-fwd

We proceed by structural induction on .
Note that for all  in the codomain of , it is either
generated by the , , or  of .  Thus, we
only need to prove the following three equations where  is in the
codomain of  and , , and , respectively.

* B@>l<@
[6]run_StateT (h_State (gen x)) (SS xs stack)[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (gen x));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

* B@>l<@
[6]run_StateT (h_State (alg x)) (SS xs stack)[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (alg x));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

* B@>l<@
[6]run_StateT (h_State (fwd x)) (SS xs stack)[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (fwd x));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

For the case , we calculate as follows:
[6]run_StateT (h_State (gen x)) (SS xs stack)[E]

[6]run_StateT (h_State (append_SS x pop_SS)) (SS xs stack)[E]

[6]run_StateT (h_State pop_SS) (SS (xs++[1.5mu x1.5mu]) stack)[E]

[6]run_StateT (h_State pop_SS) (SS (xs++η x) stack)[E]

[6]𝐝𝐨 {1.5mu p'←Var (η x);run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (gen x));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]
For the case , we proceed with a case analysis on .

[6]run_StateT (h_State (alg Fail)) (SS xs stack)[E]

[6]run_StateT (h_State pop_SS) (SS xs stack)[E]

[6]run_StateT (h_State pop_SS) (SS (xs++[1.5mu 1.5mu]) stack)[E]

[6]𝐝𝐨 {1.5mu p'←Var [1.5mu 1.5mu];run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (alg Fail));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[6]run_StateT (h_State (alg (Or p_1 p_2))) (SS xs stack)[E]

[6]run_StateT (h_State (push_SS p_2 p_1)) (SS xs stack)[E]

[6]run_StateT (h_State p_1) (SS xs (p_2:stack))[E]

[6]𝐝𝐨 {1.5mu p_1'←extract_SS (h_State p_1);run_StateT (h_State pop_SS) (SS (xs++p_1') (p_2:stack))1.5mu}[E]

[6]𝐝𝐨 {1.5mu p_1'←extract_SS (h_State p_1);run_StateT (h_State p_2) (SS (xs++p_1') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p_2'←extract_SS (h_State p_2);𝐝𝐨 {1.5mu p_1'←extract_SS (h_State p_1);[E]

[8]run_StateT (h_State pop_SS) (SS (xs++p_1'++p_2') stack)1.5mu}1.5mu}[E]

[6]𝐝𝐨 {1.5mu p_2'←extract_SS (h_State p_2);p_1'←extract_SS (h_State p_1);[E]

[8]run_StateT (h_State pop_SS) (SS (xs++p_1'++p_2') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←liftM2 (++) (extract_SS (h_State p_2)) (extract_SS (h_State p_1));[E]

[8]run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (alg (Or p_1 p_2)));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

For the case , we proceed with a case analysis on .
[6]run_StateT (h_State (fwd x)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inr x))) (SS xs stack)[E]

[6]run_StateT (StateT (λs→Op (fmap (λy→run_StateT (h_State y s)) x))) (SS xs stack)[E]

[6]Op (fmap (λy→run_StateT (h_State y (SS xs stack))) x)[E]

[5]Op (fmap (λy→𝐝𝐨 {1.5mu p'←extract_SS (h_State y);run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}) x)[E]

[5]𝐝𝐨 {1.5mu p'←Op (fmap (λy→extract_SS (h_State y)) x);run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[5]𝐝𝐨 {1.5mu p'←fwd_ND+f (fmap (λy→extract_SS (h_State y)) x);run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

[6]𝐝𝐨 {1.5mu p'←extract_SS (h_State (fwd x));run_StateT (h_State pop_SS) (SS (xs++p') stack)1.5mu}[E]

The following four lemmas characterise the behaviours of stack

[3]run_StateT (h_State (append_SS x p)) (SS xs stack)=run_StateT (h_State p) (SS (xs++[1.5mu x1.5mu]) stack)[E]

[6]run_StateT (h_State (append_SS x p)) (SS xs stack)[E]

[6]run_StateT (h_State (get>>=λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Get η))>>=λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p)) [E]

[8](SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Get (λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p))))) (SS xs stack)[E]

[6]run_StateT (StateT (λs→run_StateT (h_State ((λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p) s)) s)) [E]

[8](SS xs stack)[E]

[6](λs→run_StateT (h_State ((λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p) s)) s) (SS xs stack)[E]

[6]run_StateT (h_State ((λ(SS xs stack)→put (SS (xs++[1.5mu x1.5mu]) stack)>>p) (SS xs stack))) (SS xs stack)[E]

[6]run_StateT (h_State (put (SS (xs++[1.5mu x1.5mu]) stack)>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Put (SS (xs++[1.5mu x1.5mu]) stack) (η ())))>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Put (SS (xs++[1.5mu x1.5mu]) stack) p)))) (SS xs stack)[E]

[6]run_StateT (StateT (λs→run_StateT (h_State p) (SS (xs++[1.5mu x1.5mu]) stack))) (SS xs stack)[E]

[6](λs→run_StateT (h_State p) (SS (xs++[1.5mu x1.5mu]) stack)) (SS xs stack)[E]

[6]run_StateT (h_State p) (SS (xs++[1.5mu x1.5mu]) stack)[E]

[3]run_StateT (h_State pop_SS) (SS xs [1.5mu 1.5mu])=η ((),SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State pop_SS) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State (get>>=λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op)) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State (Op (Inl (Get η))>>=λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op)) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State (Op (Inl (Get (λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op))))) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (StateT (λs→run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) s)) s)) (SS xs [1.5mu 1.5mu])[E]

[6](λs→run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) s)) s) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) (SS xs [1.5mu 1.5mu]))) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (h_State (η ())) (SS xs [1.5mu 1.5mu])[E]

[6]run_StateT (StateT (λs→η ((),s))) (SS xs [1.5mu 1.5mu])[E]

[6](λs→η ((),s)) (SS xs [1.5mu 1.5mu])[E]

[6]((),SS xs [1.5mu 1.5mu])[E]

[3]run_StateT (h_State pop_SS) (SS xs (q:stack))=run_StateT (h_State q) (SS xs stack)[E]

[6]run_StateT (h_State pop_SS) (SS xs (q:stack))[E]

[6]run_StateT (h_State (get>>=λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op)) (SS xs (q:stack))[E]

[6]run_StateT (h_State (Op (Inl (Get η))>>=λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op)) (SS xs (q:stack))[E]

[6]run_StateT (h_State (Op (Inl (Get (λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op))))) (SS xs (q:stack))[E]

[6]run_StateT (StateT (λs→run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) s)) s)) (SS xs (q:stack))[E]

[6](λs→run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) s)) s) (SS xs (q:stack))[E]

[6]run_StateT (h_State ((λ(SS xs stack)→[E]

[8]𝐜𝐚𝐬𝐞 stack 𝐨𝐟 [23]
[23][1.5mu 1.5mu][32]
[32]→η ()[E]

[32]→𝐝𝐨 put (SS xs ps);op) (SS xs (q:stack)))) (SS xs (q:stack))[E]

[6]run_StateT (h_State (put (SS xs stack)>>q)) (SS xs (q:stack))[E]

[6]run_StateT (h_State (Op (Inl (Put (SS xs stack) (η ())))>>q)) (SS xs (q:stack))[E]

[6]run_StateT (h_State (Op (Inl (Put (SS xs stack) q)))) (SS xs (q:stack))[E]

[6]run_StateT (StateT (λs→run_StateT (h_State q) (SS xs stack))) (SS xs (q:stack))[E]

[6](λs→run_StateT (h_State q) (SS xs stack)) (SS xs (q:stack))[E]

[6]run_StateT (h_State q) (SS xs stack)[E]

[3]run_StateT (h_State (push_SS q p)) (SS xs stack)=run_StateT (h_State p) (SS xs (q:stack))[E]

[6]run_StateT (h_State (push_SS q p)) (SS xs stack)[E]

[6]run_StateT (h_State (get>>=λ(SS xs stack)→put (SS xs (q:stack))>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Get η))>>=λ(SS xs stack)→put (SS xs (q:stack))>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Get (λ(SS xs stack)→put (SS xs (q:stack))>>p))))) (SS xs stack)[E]

[6]run_StateT (StateT (λs→run_StateT (h_State ((λ(SS xs stack)→put (SS xs (q:stack))>>p) s)) s)) [E]

[8](SS xs stack)[E]

[6](λs→run_StateT (h_State ((λ(SS xs stack)→put (SS xs (q:stack))>>p) s)) s) (SS xs stack)[E]

[6]run_StateT (h_State ((λ(SS xs stack)→put (SS xs (q:stack))>>p) (SS xs stack))) (SS xs stack)[E]

[6]run_StateT (h_State (put (SS xs (q:stack))>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Put (SS xs (q:stack)) (η ())))>>p)) (SS xs stack)[E]

[6]run_StateT (h_State (Op (Inl (Put (SS xs (q:stack)) p)))) (SS xs stack)[E]

[6]run_StateT (StateT (λs→run_StateT (h_State p) (SS xs (q:stack)))) (SS xs stack)[E]

[6](λs→run_StateT (h_State p) (SS xs (q:stack))) (SS xs stack)[E]

[6]run_StateT (h_State p) (SS xs (q:stack))[E]

§ PROOFS FOR MODELLING TWO STATES WITH ONE STATE

In this section, we prove the following theorem in

Instead of proving it directly, we show the correctness of the
isomorphism of  and , and prove the following equation:B@>l<@

It is obvious that  and  form an isomorphism, i.e.,
and . We show that
and  form an isomorphism by calculation.
For all , we show that .
[6](nest∘.flatten) t[E]

[6]nest$StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (run_StateT t s_1) s_2[E]

[8]run_StateT (StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (run_StateT t s_1) s_2) (s_1,s_2)[E]

[8](λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (run_StateT t s_1) s_2) (s_1,s_2)[E]

[6]StateT$λs_1→StateT$λs_2→α^-1⟨0.1pt1$⟩(α⟨0.1pt1$⟩run_StateT (run_StateT t s_1) s_2)[E]

[6]StateT$λs_1→StateT$λs_2→(fmap (α^-1∘.α) (run_StateT (run_StateT t s_1) s_2))[E]

[6]StateT$λs_1→StateT$λs_2→(fmap id (run_StateT (run_StateT t s_1) s_2))[E]

[6]StateT$λs_1→StateT$λs_2→(run_StateT (run_StateT t s_1) s_2)[E]

[6]StateT$λs_1→(StateT∘.run_StateT) (run_StateT t s_1)[E]

[6]StateT$λs_1→run_StateT t s_1[E]

[6]StateT$run_StateT t[E]

For all , we show that .
[6](flatten∘.nest) t=t[E]

[6]flatten$StateT$λs_1→StateT$λs_2→α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2)[E]

[8]run_StateT (run_StateT (StateT$λs_1→StateT$λs_2→α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2)) s_1) s_2[E]

[8]run_StateT ((λs_1→StateT$λs_2→α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2)) s_1) s_2[E]

[6]StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (StateT$λs_2→α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2)) s_2[E]

[6]StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩(λs_2→α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2)) s_2[E]

[6]StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩(α^-1⟨0.1pt1$⟩run_StateT t (s_1,s_2))[E]

[6]StateT$λ(s_1,s_2)→fmap α (fmap α^-1 (run_StateT t (s_1,s_2)))[E]

[6]StateT$λ(s_1,s_2)→fmap (α∘.α^-1) (run_StateT t (s_1,s_2))[E]

[6]StateT$λ(s_1,s_2)→fmap id (run_StateT t (s_1,s_2))[E]

[6]StateT$λ(s_1,s_2)→run_StateT t (s_1,s_2)[E]

[6]StateT$run_StateT t[E]

Then, we first calculate the LHS  into one function
which is defined asB@>l<@
[3]h_States^'::Functor f⇒Free (State_F s_1:+:State_F s_2:+:f) a→StateT (s_1,s_2) (Free f) a[E]

[3]h_States^' t=StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2[E]

For all , we show the equation
by the following calculation.
[6](flatten∘.h_States) t[E]

[6](flatten∘.(λt→StateT (h_State∘.run_StateT (h_State t)))) t[E]

[6]flatten (StateT (h_State∘.run_StateT (h_State t)))[E]

[8]run_StateT (run_StateT (StateT (h_State∘.run_StateT (h_State t))) s_1) s_2[E]

[8]run_StateT ((h_State∘.run_StateT (h_State t)) s_1) s_2[E]

[3]h_States^' t[E]
Now we only need to show that for any input , the equation  holds.
Note that both sides use folds.
We can proceed with either fold fusion, as what we have done in the
proofs of other theorems, or a direct structural induction on the
input . Although using fold fusion makes the proof simpler than
using structural induction, we opt for the latter here to show that
the our methods of defining effects and translations based on
algebraic effects and handlers also work well with structural

[6](h_State∘.states2state) (Var x)[E]

[6]h_State (Var x)[E]

[5]StateT$λs→η (x,s)[E]

[6]StateT$λ(s_1,s_2)→Var (x,(s_1,s_2))[E]

[31]Var (α ((x,s_1),s_2))[E]

[31]fmap α$Var ((x,s_1),s_2)[E]

[31]fmap α$η ((x,s_1),s_2)[E]

[31]fmap α$(λs→η ((x,s_1),s)) s_2[E]

[31]fmap α$run_StateT (StateT$λs→η ((x,s_1),s)) s_2[E]

[31]fmap α$run_StateT (h_State (η (x,s_1))) s_2[E]

[31]fmap α$run_StateT (h_State ((λs→η (x,s)) s_1)) s_2[E]

[31]fmap α$run_StateT (h_State (run_StateT (StateT$λs→η (x,s)) s_1)) s_2[E]

[31]fmap α$run_StateT (h_State (run_StateT (h_State (Var x)) s_1)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State (Var x)) s_1)) s_2[E]

[6]h_States^' (Var x)[E]

Induction hypothesis:  for any .
[6](h_State∘.states2state) (Op (Inl (Get k)))[E]

[31])→states2state (k s_1)[E]

[6]h_State$Op (Inl (Get η))>>=λ(s_1,)→states2state (k s_1)[E]

[6]h_State (Op (Inl (Get (λ(s_1,)→states2state (k s_1)))))[E]

[6]StateT$λs→run_StateT ((λ(s_1,)→h_State (states2state (k s_1))) s) s[E]

[6]StateT$λ(s_1,s_2)→run_StateT ((λ(s_1,)→h_State (states2state (k s_1))) (s_1,s_2)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_State (states2state (k s_1))) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_States^' (k s_1)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (StateT$λ(s_1,s_2)[61]

[8]run_StateT (h_State (run_StateT (h_State (k s_1)) s_1)) s_2) (s_1,s_2)[E]

[8]run_StateT (h_State (run_StateT (h_State (k s_1)) s_1)) s_2) (s_1,s_2)[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State (k s_1)) s_1)) s_2[E]

[8]run_StateT (h_State ((λs→run_StateT (h_State (k s)) s) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (StateT$λs→run_StateT (h_State (k s)) s) s_1)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State (Op (Inl (Get k)))) s_1)) s_2[E]

[6]h_States^' (Op (Inl (Get k)))[E]

Induction hypothesis: .
[6](h_State∘.states2state) (Op (Inl (Put s k)))[E]

[34]→put (s,s_2)>>(states2state k)[E]

[6]h_State$Op (Inl (Get η))>>=λ(,s_2)→Op (Inl (Put (s,s_2) (η ())))>>(states2state k)[E]

[6]h_State$Op (Inl (Get (λ(,s_2)→Op (Inl (Put (s,s_2) (states2state k))))))[E]

[6]alg_S (Get (λ(,s_2)→h_State (Op (Inl (Put (s,s_2) (states2state k))))))[E]

[8]((λ(,s_2)→h_State (Op (Inl (Put (s,s_2) (states2state k))))) s') s'[E]

[8]((λ(,s_2)→h_State (Op (Inl (Put (s,s_2) (states2state k))))) (s_1,s_2)) (s_1,s_2)[E]

[8](h_State (Op (Inl (Put (s,s_2) (states2state k))))) (s_1,s_2)[E]

[8](StateT$λ→run_StateT (h_State (states2state k)) (s,s_2)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→(λ→run_StateT (h_State (states2state k)) (s,s_2)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_State (states2state k)) (s,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_States^' k) (s,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩[E]

[9]run_StateT (h_State (run_StateT (h_State k) s_1)) s_2) (s,s_2)[E]

[8]run_StateT (h_State (run_StateT (h_State k) s_1)) s_2) (s,s_2)[E]

[8]run_StateT (h_State (run_StateT (h_State k) s)) s_2[E]

[8]run_StateT (h_State ((λs'→run_StateT (h_State k) s) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (StateT$λs'→run_StateT (h_State k) s) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (h_State (Op (Inl (Put s k)))) s_1)) s_2[E]

[6]h_States^' (Op (Inl (Put s k)))[E]

Induction hypothesis:
for any .
[6](h_State∘.states2state) (Op (Inr (Inl (Get k))))[E]

[30]s_2)→states2state (k s_2)[E]

[6]h_State$Op (Inl (Get η))>>=λ(,s_2)→states2state (k s_2)[E]

[6]h_State (Op (Inl (Get (λ(,s_2)→states2state (k s_2)))))[E]

[6]StateT$λs→run_StateT ((λ(,s_2)→h_State (states2state (k s_2))) s) s[E]

[6]StateT$λ(s_1,s_2)→run_StateT ((λ(,s_2)→h_State (states2state (k s_2))) (s_1,s_2)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_State (states2state (k s_2))) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_States^' (k s_2)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (StateT$λ(s_1,s_2)[61]

[8]run_StateT (h_State (run_StateT (h_State (k s_2)) s_1)) s_2) (s_1,s_2)[E]

[8]run_StateT (h_State (run_StateT (h_State (k s_2)) s_1)) s_2) (s_1,s_2)[E]

[8]run_StateT (h_State (run_StateT (h_State (k s_2)) s_1)) s_2[E]

[8](run_StateT ((h_State∘.(λk→run_StateT k s_1)∘.h_State∘.k) s_2) s_2)[E]

[8](λs→run_StateT ((h_State∘.(λk→run_StateT k s_1)∘.h_State∘.k) s) s) s_2[E]

[8]run_StateT (StateT$λs→run_StateT ((h_State∘.(λk→run_StateT k s_1)∘.h_State∘.k) s) s) s_2[E]

[8]run_StateT (h_State (Op (Inl (Get ((λk→run_StateT k s_1)∘.h_State∘.k))))) s_2[E]

[8]run_StateT (h_State (Op$fmap (λk→run_StateT k s_1) (Inl (Get (h_State∘.k))))) s_2[E]

[8]run_StateT (h_State ((λs→Op$fmap (λk→run_StateT k s) (Inl (Get (h_State∘.k)))) s_1)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State[E]

[8](run_StateT (StateT$λs→Op$fmap (λk→run_StateT k s) (Inl (Get (h_State∘.k)))) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (h_State (Op (Inr (Inl (Get k))))) s_1)) s_2[E]

[6]h_States^' (Op (Inr (Inl (Get k))))[E]

Induction hypothesis: .
[6](h_State∘.states2state) (Op (Inr (Inl (Put s k))))[E]

[6]h_State$get>>=λ(s_1,)→put (s_1,s)>>(states2state k)[E]

[6]h_State$Op (Inl (Get η))>>=λ(s_1,)→Op (Inl (Put (s_1,s) (η ())))>>(states2state k)[E]

[6]h_State$Op (Inl (Get (λ(s_1,)→Op (Inl (Put (s_1,s) (states2state k))))))[E]

[8]((λ(s_1,)→h_State (Op (Inl (Put (s_1,s) (states2state k))))) s') s'[E]

[8]((λ(s_1,)→h_State (Op (Inl (Put (s_1,s) (states2state k))))) (s_1,s_2)) (s_1,s_2)[E]

[8](h_State (Op (Inl (Put (s_1,s) (states2state k))))) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (StateT$[E]

[8]λs'→run_StateT (h_State (states2state k)) (s_1,s)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→(λs'→run_StateT (h_State (states2state k)) (s_1,s)) (s_1,s_2)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_State (states2state k)) (s_1,s)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (h_States^' k) (s_1,s)[E]

[6]StateT$λ(s_1,s_2)→run_StateT (StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩[E]

[8]run_StateT (h_State (run_StateT (h_State k) s_1)) s_2) (s_1,s)[E]

[8]run_StateT (h_State (run_StateT (h_State k) s_1)) s_2) (s_1,s)[E]

[8]run_StateT (h_State (run_StateT (h_State k) s_1)) s[E]

[8](λs'→run_StateT (h_State (run_StateT (h_State k) s_1)) s) s_2[E]

[8]run_StateT (StateT$λs'→run_StateT (h_State (run_StateT (h_State k) s_1)) s) s_2[E]

[8]run_StateT (h_State (Op (Inl (Put s (run_StateT (h_State k) s_1))))) s_2[E]

[8]run_StateT (h_State (Op (Inl (Put s ((λk→run_StateT k s_1) (h_State k)))))) s_2[E]

[8]run_StateT (h_State (Op$fmap (λk→run_StateT k s_1) (Inl (Put s (h_State k))))) s_2[E]

[8](h_State ((λs'→Op$fmap (λk→run_StateT k s') (Inl (Put s (h_State k)))) s_1)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (StateT$[E]

[8]λs'→Op$fmap (λk→run_StateT k s') (Inl (Put s (h_State k)))) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (h_State (Op (Inr (Inl (Put s k))))) s_1)) s_2[E]

[6]h_States^' (Op (Inr (Inl (Put s k))))[E]

Induction hypothesis: .
[6](h_State∘.states2state) (Op (Inr (Inr y)))[E]

[6]h_State$Op (Inr (fmap states2state y))[E]

[6]fwd_S (fmap (h_State∘.states2state) y)[E]

[6]fwd_S (fmap h_States^' y)[E]

[6]fwd_S (fmap (λt→StateT[E]

[26]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) y)[E]

[6]StateT$λs→Op$fmap (λk→run_StateT k s) (fmap (λt→StateT[E]

[8]$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) y)[E]

[6]StateT$λs→Op (fmap ((λk→run_StateT k s)∘.(λt→StateT[E]

[8]$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2)) y)[E]

[6]StateT$λs→Op (fmap (λt→run_StateT (StateT[E]

[8]$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) s) y)[E]

[6]StateT$λs→Op (fmap (λt→[E]

[8](λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) s) y)[E]

[6]StateT$λ(s_1,s_2)→Op (fmap (λt→[E]

[8](λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) (s_1,s_2)) y)[E]

[6]StateT$λ(s_1,s_2)→Op (fmap (λt→α⟨0.1pt1$⟩[E]

[9]run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) y)[E]

[6]StateT$λ(s_1,s_2)→Op (fmap (α⟨0.1pt1$⟩[E]

[8]∘.(λk→run_StateT k s_2)∘.h_State∘.(λk→run_StateT k s_1)∘.h_State) y)[E]

[8]Op (fmap ((λk→run_StateT k s_2)∘.h_State∘.(λk→run_StateT k s_1)∘.h_State) y)[E]

[8]Op$fmap (λk→run_StateT k s_2) (fmap (h_State∘.(λk→run_StateT k s_1)∘.h_State) y)[E]

[8]fmap (λk→run_StateT k s) (fmap (h_State∘.(λk→run_StateT k s_1)∘.h_State) y)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (StateT$λs→Op$[E]

[8]fmap (λk→run_StateT k s) (fmap (h_State∘.(λk→run_StateT k s_1)∘.h_State) y)) s_2[E]

[8](h_State (Op (Inr (fmap ((λk→run_StateT k s_1)∘.h_State) y)))) s_2[E]

[8](h_State (Op (Inr (fmap (λk→run_StateT k s_1) (fmap h_State y))))) s_2[E]

[8](h_State (Op$fmap (λk→run_StateT k s_1) (Inr (fmap h_State y)))) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State[E]

[8]((λs→Op$fmap (λk→run_StateT k s) (Inr (fmap h_State y))) s_1)) s_2[E]

[31]α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (StateT$[E]

[8]λs→Op$fmap (λk→run_StateT k s) (Inr (fmap h_State y))) s_1)) s_2[E]

[8]run_StateT (h_State (run_StateT (h_State (Op (Inr (Inr y)))) s_1)) s_2[E]

[6]h_States^' (Op (Inr (Inr y)))[E]

§ PROOFS FOR THE ALL IN ONE SIMULATION

In this section, we prove the correctness of the final simulation in

We calculate as follows, using all our three previous theorems
<Ref>, <Ref>,
<Ref>, and an auxiliary lemma <Ref>.

[6]fmap (fmap fst)∘.run_StateT∘.h_State∘.extract_SS∘.h_State∘.nondet2state∘.(⇔)∘.local2global[E]

[6]fmap (fmap fst)∘.run_StateT∘.h_State∘.run_ND+f∘.(⇔)∘.local2global[E]

[6]fmap (fmap fst)∘.run_StateT∘.h_State∘.h_ND+f∘.(⇔)∘.local2global[E]

[6]extract∘.flatten∘.h_States=fmap (fmap fst)∘.run_StateT∘.h_State∘.extract_SS∘.h_State[E]

As shown in <Ref>, we can combine  into one function  defined as follows:B@>l<@
[3]h_States^'::Functor f⇒Free (State_F s_1:+:State_F s_2:+:f) a→StateT (s_1,s_2) (Free f) a[E]

[3]h_States^' t=StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) s_1)) s_2[E]
Then we show that for any input , we have  via the
following calculation.
[6](extract∘.h_States^') t[E]

[6]extract (h_States^' t)[E]

[6]extract (StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩[E]

[8]run_StateT (h_State (run_StateT (h_State t) s_1)) s_2)[E]

[6]λs→results_SS∘.fst∘.snd⟨0.1pt1$⟩run_StateT (StateT$λ(s_1,s_2)→α⟨0.1pt1$⟩[E]

[8]run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) (SS [1.5mu 1.5mu] [1.5mu 1.5mu],s)[E]

[8]run_StateT (h_State (run_StateT (h_State t) s_1)) s_2) (SS [1.5mu 1.5mu] [1.5mu 1.5mu],s)[E]

[8]run_StateT (h_State (run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))) s)[E]

[8]run_StateT (h_State (run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))) s[E]

[6]λs→results_SS∘.snd∘.fst⟨0.1pt1$⟩run_StateT (h_State (run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))) s[E]

[6]λs→fmap (results_SS∘.snd)∘.fmap fst$[E]

[8]run_StateT (h_State (run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))) s[E]

[6]λs→fmap (results_SS∘.snd)∘.fmap fst$[E]

[8]flip (run_StateT∘.h_State) s (run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))[E]

[6]λs→fmap (results_SS∘.snd)∘.(fmap fst∘.flip (run_StateT∘.h_State) s)$[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]λs→(fmap fst∘.flip (run_StateT∘.h_State) s)∘.fmap (results_SS∘.snd)$[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]λs→(fmap fst∘.flip (run_StateT∘.h_State) s)$results_SS∘.snd⟨0.1pt1$⟩[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]λs→fmap fst (run_StateT (h_State (results_SS∘.snd⟨0.1pt1$⟩[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu]))) s)[E]

[6]λs→fmap (fmap fst) (run_StateT (h_State (results_SS∘.snd⟨0.1pt1$⟩[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])))) s[E]

[6]λs→(fmap (fmap fst)∘.run_StateT∘.h_State$results_SS∘.snd⟨0.1pt1$⟩[E]

[8]run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])) s[E]

[6]fmap (fmap fst)∘.run_StateT∘.h_State$results_SS∘.snd⟨0.1pt1$⟩run_StateT (h_State t) (SS [1.5mu 1.5mu] [1.5mu 1.5mu])[E]

[6]fmap (fmap fst)∘.run_StateT∘.h_State$extract_SS (h_State t)[E]

[6](fmap (fmap fst)∘.run_StateT∘.h_State∘.extract_SS∘.h_State) t[E]
Note that in the above calculation, we use the
parametricity [Reynolds, 1983, Wadler, 1989] of free monads which is
formally stated as follows:B@>l<@
[3]fmap f∘.g=g∘.fmap f[E]
for any  with two functors
and .

§ PROOFS FOR MODELLING LOCAL STATE WITH UNDO

In this section, we prove the following theorem in <Ref>.

The proof structure is very similar to that in
<Ref>. We start with the following preliminary

It is easy to see that  can be fused into a single
fold defined as follows:
[11]::(Functor f,Undo s r)⇒Free (Modify_F s r:+:f) a→(s→Free f (a,s))[E]

[14]fold gen_S (alg_S#fwd_S)[E]

[5]gen_S x [26]
[26]s=Var (x,s)[E]

[5]alg_S (MGet k) [26]
[26]s=k s s[E]

[5]alg_S (MUpdate r k) [26]
[26]s=k (s⊕r)[E]

[5]alg_S (MRestore r k) [26]
[26]s=k (s⊖r)[E]

[5]fwd_S y [26]
[26]s=Op (fmap ($s) y)[E]
For brevity, we use  to replace  in the
following proofs.

§.§ Main Proof Structure

The main proof structure of <Ref> is as

Both the left-hand side and the right-hand side of the equation consist of
function compositions involving one or more folds.
We apply fold fusion separately on both sides to contract each
into a single fold:

\begin{eqnarray*}
\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{local2global_M}} & = & \ensuremath{\Varid{fold}\;\Varid{gen}_{\Varid{LHS}}\;(\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{LHS}})} \\
\ensuremath{\Varid{h_{LocalM}}}& = & \ensuremath{\Varid{fold}\;\Varid{gen}_{\Varid{RHS}}\;(\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{RHS}})}
\end{eqnarray*}

Finally, we show that both folds are equal by showing that their
corresponding parameters are equal:

\begin{eqnarray*}
\ensuremath{\Varid{gen}_{\Varid{LHS}}} & = & \ensuremath{\Varid{gen}_{\Varid{RHS}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}} \\
\ensuremath{\Varid{fwd}_{\Varid{LHS}}} & = & \ensuremath{\Varid{fwd}_{\Varid{RHS}}}
\end{eqnarray*}

We elaborate each of these steps below.

§.§ Fusing the Right-Hand Side

We calculate as follows:

[7] with  [E]

[14]::(Functor f,Functor g)[E]

[14]⇒g (Free (Nondet_F:+:f) (a,s))→g (Free f [1.5mu a1.5mu])[E]

[14]=fmap (fmap (fmap fst)∘.h_ND+f)[E]

[5]h_L∘.fold gen_S (alg_S#fwd_S)[E]

[5]fold gen_RHS (alg_RHS^S#alg_RHS^ND#fwd_RHS)[E]
This last step is valid provided that the fusion conditions are satisfied:

\[\ba{rclr}
\ensuremath{\Varid{h_{L}}\hsdot{\circ }{.}\Varid{gen_{S}}} & = & \ensuremath{\Varid{gen}_{\Varid{RHS}}} &\refa{} \\
\ensuremath{\Varid{h_{L}}\hsdot{\circ }{.}(\Varid{alg_{S}}\mathbin{\#}\Varid{fwd_{S}})} & = & \ensuremath{(\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{RHS}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{L}}} &\refb{}
\ea\]

For the first fusion condition , we define  as followsB@>l<@
[3]gen_RHS::Functor f⇒a→(s→Free f [1.5mu a1.5mu])[E]

[3]gen_RHS x=λs→Var [1.5mu x1.5mu][E]
We show that  is satisfied by the following calculation.
[5]h_L (gen_S x)[E]

[5]h_L (λs→Var (x,s))[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→Var (x,s))[E]

[5]λs→fmap (fmap fst) (h_ND+f (Var (x,s)))[E]

[5]λs→fmap (fmap fst) (Var [1.5mu (x,s)1.5mu])[E]

[5]λs→Var [1.5mu x1.5mu][E]

[3]=gen_RHS x[E]
By a straightforward case analysis on the two cases  and ,
the second fusion condition  decomposes into two separate

\[\ba{rclr}
\ensuremath{\Varid{h_{L}}\hsdot{\circ }{.}\Varid{alg_{S}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{L}}} &\refc{} \\
\ensuremath{\Varid{h_{L}}\hsdot{\circ }{.}\Varid{fwd_{S}}\hsdot{\circ }{.}\Conid{Inl}}& = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{L}}} &\refd{}\\
\ensuremath{\Varid{h_{L}}\hsdot{\circ }{.}\Varid{fwd_{S}}\hsdot{\circ }{.}\Conid{Inr}}& = & \ensuremath{\Varid{fwd}_{\Varid{RHS}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{L}}} &\refe{}
\ea\]

For the subcondition , we define  as follows.B@>l<@
[3]alg_RHS^S::Undo s r⇒Modify_F s r (s→p)→(s→p)[E]

[3]alg_RHS^S (MGet k)[27]
[27]=λs→k s s[E]

[3]alg_RHS^S (MUpdate r k)[27]
[27]=λs→k (s⊕r)[E]

[3]alg_RHS^S (MRestore r k)[27]
[27]=λs→k (s⊕r)[E]
We prove its correctness by a case analysis on the shape of input .

[5]h_L (alg_S (Get k))[E]

[5]h_L (λs→k s s)[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→k s s)[E]

[5]λs→fmap (fmap fst) (h_ND+f (k s s))[E]

[3]=λs→(λs_1 s_2→fmap (fmap fst) (h_ND+f (k s_2 s_1))) s s[E]

[3]=λs→(fmap (fmap (fmap (fmap fst)∘.h_ND+f)) (λs_1 s_2→k s_2 s_1)) s s[E]

[3]=λs→(fmap (fmap (fmap (fmap fst)∘.h_ND+f)) k) s s[E]

[3]=alg_RHS^S (Get (fmap (fmap (fmap (fmap fst)∘.h_ND+f)) k))[E]

[3]=alg_RHS^S (fmap (fmap (fmap (fmap fst)∘.h_ND+f)) (Get k))[E]

[3]=alg_RHS^S (fmap h_L (Get k))[E]
[5]h_L (alg_S (MUpdate r k))[E]

[5]h_L (λs→k (s⊕r))[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→k (s⊕r))[E]

[5]λs→fmap (fmap fst) (h_ND+f (k (s⊕r)))[E]

[3]=λs→(λs_1→fmap (fmap fst) (h_ND+f (k s_1))) (s⊕r)[E]

[3]=λs→(fmap (fmap (fmap fst)∘.h_ND+f) (λs_1→k s_1)) (s⊕r)[E]

[3]=λs→(fmap (fmap (fmap fst)∘.h_ND+f) k) (s⊕r)[E]

[3]=alg_RHS^S (MUpdate r (fmap (fmap (fmap fst)∘.h_ND+f) k))[E]

[3]=alg_RHS^S (fmap (fmap (fmap fst)∘.h_ND+f)) (MUpdate r k))[E]

[3]=alg_RHS^S (fmap h_L (MUpdate r k))[E]
[5]h_L (alg_S (MRestore r k))[E]

[5]h_L (λs→k (s⊖r))[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→k (s⊖r))[E]

[5]λs→fmap (fmap fst) (h_ND+f (k (s⊖r)))[E]

[3]=λs→(λs_1→fmap (fmap fst) (h_ND+f (k s_1))) (s⊖r)[E]

[3]=λs→(fmap (fmap (fmap fst)∘.h_ND+f) (λs_1→k s_1)) (s⊖r)[E]

[3]=λs→(fmap (fmap (fmap fst)∘.h_ND+f) k) (s⊖r)[E]

[3]=alg_RHS^S (MRestore r (fmap (fmap (fmap fst)∘.h_ND+f) k))[E]

[3]=alg_RHS^S (fmap (fmap (fmap fst)∘.h_ND+f)) (MRestore r k))[E]

[3]=alg_RHS^S (fmap h_L (MRestore r k))[E]

For the subcondition , we define  as follows.B@>l<@
[3]alg_RHS^ND::Functor f⇒Nondet_F (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]alg_RHS^ND Fail[22]
[22]=λs→Var [1.5mu 1.5mu][E]

[3]alg_RHS^ND (Or p q)[22]
[22]=λs→liftM2 (++) (p s) (q s)[E]
To show its correctness, given  with , we calculate:
[5]h_L (fwd_S (Inl op))[E]

[5]h_L (λs→Op (fmap ($s) (Inl op)))[E]

[5]h_L (λs→Op (Inl (fmap ($s) op)))[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→Op (Inl (fmap ($s) op)))[E]

[5]λs→fmap (fmap fst) (h_ND+f (Op (Inl (fmap ($s) op))))[E]

[5]λs→fmap (fmap fst) (alg_ND+f (fmap h_ND+f (fmap ($s) op)))[E]
We proceed by a case analysis on :

[5]λs→fmap (fmap fst) (alg_ND+f (fmap h_ND+f (fmap ($s) Fail)))[E]

[5]λs→fmap (fmap fst) (alg_ND+f Fail)[E]

[5]λs→fmap (fmap fst) (Var [1.5mu 1.5mu])[E]

[5]λs→Var [1.5mu 1.5mu][E]

[5]alg_RHS^ND Fail[E]

[5]alg_RHS^ND (fmap h_L fail)[E]
[5]λs→fmap (fmap fst) (alg_ND+f (fmap h_ND+f (fmap ($s) (Or p q))))[E]

[5]λs→fmap (fmap fst) (alg_ND+f (Or (h_ND+f (p s)) (h_ND+f (q s))))[E]

[5]λs→fmap (fmap fst) (liftM2 (++) (h_ND+f (p s)) (h_ND+f (q s)))[E]

[5]λs→liftM2 (++) (fmap (fmap fst) (h_ND+f (p s))) (fmap (fmap fst) (h_ND+f (q s)))[E]

[5]alg_RHS^ND (Or (fmap (fmap fst)∘.h_ND+f∘.p) (fmap (fmap fst)∘.h_ND+f∘.q))[E]

[5]alg_RHS^ND (fmap (fmap (fmap (fmap fst)∘.h_ND+f)) (Or p q))[E]

[5]alg_RHS^ND (fmap h_L (Or p q))[E]

For the last subcondition , we define  as follows.B@>l<@
[3]fwd_RHS::Functor f⇒f (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]fwd_RHS op=λs→Op (fmap ($s) op)[E]
To show its correctness, given input , we calculate:
[5]h_L (fwd_S (Inr op))[E]

[5]h_L (λs→Op (fmap ($s) (Inr op)))[E]

[5]h_L (λs→Op (Inr (fmap ($s) op)))[E]

[5]fmap (fmap (fmap fst)∘.h_ND+f) (λs→Op (Inr (fmap ($s) op)))[E]

[5]λs→fmap (fmap fst) (h_ND+f (Op (Inr (fmap ($s) op))))[E]

[5]λs→fmap (fmap fst) (fwd_ND+f (fmap h_ND+f (fmap ($s) op)))[E]

[5]λs→fmap (fmap fst) (Op (fmap h_ND+f (fmap ($s) op)))[E]

[5]λs→Op (fmap (fmap (fmap fst)) (fmap h_ND+f (fmap ($s) op)))[E]

[5]λs→Op (fmap (fmap (fmap fst)∘.h_ND+f) (fmap ($s) op))[E]

[5]λs→Op (h_L (fmap ($s) op))[E]

[5]λs→Op (fmap (($s)∘.h_L) op)[E]

[5]λs→Op (fmap ($s) (fmap h_L op))[E]

[5]fwd_RHS (fmap h_L op)[E]

§.§ Fusing the Left-Hand Side

We calculate as follows:

[5]h_GlobalM∘.fold Var alg[E]

[9]alg (Inl (MUpdate r k))[34]
[34]=(update rside (restore r))>>k[E]

[9]alg p[34]
[34]=Op p[E]

[5]fold gen_LHS (alg_LHS^S#alg_LHS^ND#fwd_LHS)[E]
This last step is valid provided that the fusion conditions are satisfied:

\[\ba{rclr}
\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Conid{Var}} & = & \ensuremath{\Varid{gen}_{\Varid{LHS}}} &\refa{}\\
\ea\]

\[\ba{rlr}
&\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} \\
= & \ensuremath{(\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{LHS}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} &\refb{}
\ea\]

The first subcondition  is met byB@>l<@
[3]gen_LHS::Functor f⇒a→(s→Free f [1.5mu a1.5mu])[E]

[3]gen_LHS x=λs→Var [1.5mu x1.5mu][E]
as established in the following calculation:B@>l<@
[5]h_GlobalM (Var x)[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Var x))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Var x)))[E]

[5]fmap (fmap fst) (h_Modify1 (Var [1.5mu x1.5mu]))[E]

[5]fmap (fmap fst) (λs→Var ([1.5mu x1.5mu],s))[E]

[5]λs→Var [1.5mu x1.5mu][E]

[5]gen_LHS x[E]
We can split the second fusion condition  in three

\[\ba{rclr}
\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}\hsdot{\circ }{.}\Conid{Inl}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} & = & \ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} &\refc{}\\
\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}\hsdot{\circ }{.}\Conid{Inr}\hsdot{\circ }{.}\Conid{Inl}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} & = & \ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} &\refd{}\\
\ensuremath{\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}\hsdot{\circ }{.}\Conid{Inr}\hsdot{\circ }{.}\Conid{Inr}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} & = & \ensuremath{\Varid{fwd}_{\Varid{LHS}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2global_M}} &\refe{}
\ea\]

For brevity, we omit the last common part  of
these equations in the following proofs. Instead, we assume that the
input is in the codomain of .
Also, we use the condition in <Ref> that the
input program does not use the  operation.

For the first subcondition , we can define  as follows.B@>l<@
[3]alg_LHS^S::(Functor f,Undo s r)⇒Modify_F s r (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]alg_LHS^S (MGet k)[27]
[30]λs→k s s[E]

[3]alg_LHS^S (MUpdate r k)[27]
[27]=λs→k (s⊕r)[E]

[3]alg_LHS^S (MRestore r k)[27]
[27]=λs→k (s⊖r)[E]
We prove it by a case analysis on the shape of input .
Note that we only need to consider the case that  is of form  or  where  is also not used in the
continuation .

[5]h_GlobalM (alg (Inl (MGet k)))[E]

[5]h_GlobalM (Op (Inl (MGet k)))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Op (Inl (MGet k))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inr (Inl (fmap (⇔) (MGet k)))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inr (Inl (MGet ((⇔)∘.k)))))))[E]

[5]fmap (fmap fst) (h_Modify1 (Op (fmap h_ND+f (Inl (MGet ((⇔)∘.k))))))[E]

[5]fmap (fmap fst) (h_Modify1 (Op (Inl (MGet (h_ND+f∘.(⇔)∘.k)))))[E]

[5]fmap (fmap fst) (λs→(h_Modify1∘.h_ND+f∘.(⇔)∘.k) s s)[E]

[5]λs→fmap fst ((h_Modify1∘.h_ND+f∘.(⇔)∘.k) s s)[E]

[5]λs→((fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.k) s s)[E]

[5]λs→(h_GlobalM∘.k) s s[E]

[5]alg_LHS^S (MGet (h_GlobalM∘.k))[E]

[5]alg_LHS^S (fmap h_GlobalM (MGet k))[E]

From  is in the codomain of  we obtain  is
in the codomain of .
[5]h_GlobalM (alg (Inl (MUpdate r k)))[E]

[5]h_GlobalM ((update rside (restore r))>>k)[E]

[5]h_GlobalM (Op (Inr (Inl (Or [33]
[33](Op (Inl (MUpdate r k))) [E]

[33](Op (Inl (MRestore r (Op (Inr (Inl Fail))))))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔)[E]

[7](Op (Inr (Inl (Or [26]
[26](Op (Inl (MUpdate r k))) [E]

[26](Op (Inl (MRestore r (Op Inr ((Inl Fail)))))))))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ([E]

[7](Op (Inl (Or [21]
[21](Op (Inr (Inl (MUpdate r ((⇔) k))))) [E]

[21](Op (Inr (Inl (MRestore r (Op (Inl Fail))))))))))))[E]

[5]fmap (fmap fst) (h_Modify1 ([E]

[7](liftM2 (++) [21]
[21](Op (Inl (MUpdate r (h_ND+f ((⇔) k))))) [E]

[21](Op (Inl (MRestore r (Var [1.5mu 1.5mu])))))))[E]

[5]fmap (fmap fst) (h_Modify1 ([E]

[7]𝐝𝐨 [11]
[11]x←Op (Inl (MUpdate r (h_ND+f ((⇔) k))))[E]

[11]y←Op (Inl (MRestore r (Var [1.5mu 1.5mu])))[E]

[11]Var (x++y)[E]

[5]fmap (fmap fst) (λt→[E]

[7]𝐝𝐨 [11]
[11](x,t_1)←h_Modify1 (Op (Inl (MUpdate r (h_ND+f ((⇔) k))))) t[E]

[11](y,t_2)←h_Modify1 (Op (Inl (MRestore r (Var [1.5mu 1.5mu])))) t_1[E]

[11]h_Modify1 (Var (x++y)) t_2[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[26]←h_Modify1 (h_ND+f ((⇔) k)) (t⊕r)[E]

[26]←Var ([1.5mu 1.5mu],t⊖r)[E]

[18]Var (x++y,t_2)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18](x,t_1)←h_Modify1 (h_ND+f ((⇔) k)) (t⊕r)[E]

[18]Var (x++[1.5mu 1.5mu],t_1⊖r)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18](x,t_1)←h_Modify1 (h_ND+f ((⇔) k)) (t⊕r)[E]

[18]Var (x,t_1⊖r)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18](x,t⊕r)←h_Modify1 (h_ND+f ((⇔) k)) (t⊕r)[E]

[18]Var (x,(t⊕r)⊖r)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18](x,)←h_Modify1 (h_ND+f ((⇔) k)) (t⊕r)[E]

[18]Var (x,t)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18]x←fmap fst (h_Modify1 (h_ND+f ((⇔) k)) (t⊕r))[E]

[18]Var (x,t)[E]

[5]fmap (fmap fst) [E]

[7](λt→𝐝𝐨 [18]
[18]x←(fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) k)))) (t⊕r)[E]

[18]Var (x,t)[E]

[5]λt→𝐝𝐨 [16]
[16]x←(fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) k)))) (t⊕r)[E]

[16]Var x[E]

[5]λt→(fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) k)))) (t⊕r)[E]

[5]λt→(h_GlobalM k) (t⊕r)[E]

[5]alg_LHS^S (MUpdate r (h_GlobalM k))[E]

[5]alg_LHS^S (fmap h_GlobalM (MUpdate r k))[E]
For the second subcondition , we can define  as
[3]alg_LHS^ND::Functor f⇒Nondet_F (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]alg_LHS^ND Fail[22]
[22]=λs→Var [1.5mu 1.5mu][E]

[3]alg_LHS^ND (Or p q)[22]
[22]=λs→liftM2 (++) (p s) (q s)[E]
We prove it by a case analysis on the shape of input .

[5]h_GlobalM (alg (Inr (Inl Fail)))[E]

[5]h_GlobalM (Op (Inr (Inl Fail)))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inl Fail))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inl (fmap (⇔) Fail)))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inl Fail))))[E]

[5]fmap (fmap fst) (h_Modify1 (Var [1.5mu 1.5mu]))[E]

[5]fmap (fmap fst) (λs→Var ([1.5mu 1.5mu],s))[E]

[5]λs→Var [1.5mu 1.5mu][E]

[4]alg_RHS^ND Fail[E]

[4]alg_RHS^ND (fmap h_GlobalM Fail)[E]

From  is in the codomain of  we obtain  and
are in the codomain of .
[5]h_GlobalM (alg (Inr (Inl (Or p q))))[E]

[5]h_GlobalM (Op (Inr (Inl (Or p q))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inl (Or p q)))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inl (fmap (⇔) (Or p q))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inl (Or ((⇔) p) ((⇔) q))))))[E]

[5]fmap (fmap fst) (h_Modify1 (liftM2 (++) (h_ND+f ((⇔) p)) (h_ND+f ((⇔) q))))[E]

[5]fmap (fmap fst) (h_Modify1 (𝐝𝐨 [36]
[36]x←h_ND+f ((⇔) p)[E]

[36]y←h_ND+f ((⇔) q)[E]

[36]η (x++y)))[E]

[5]fmap (fmap fst) (λs_0→(𝐝𝐨 [33]
[33](x,s_1)←h_Modify1 (h_ND+f ((⇔) p)) s_0[E]

[33](y,s_2)←h_Modify1 (h_ND+f ((⇔) q)) s_1[E]

[33]h_Modify1 (η (x++y)) s_2))[E]

[5]fmap (fmap fst) (λs_0→(𝐝𝐨 [33]
[33](x,s_1)←h_Modify1 (h_ND+f ((⇔) p)) s_0[E]

[33](y,s_2)←h_Modify1 (h_ND+f ((⇔) q)) s_1[E]

[33]Var (x++y,s_2)))[E]

[5]fmap (fmap fst) (λs_0→(𝐝𝐨 [33]
[33](x,s_1)←𝐝𝐨 {1.5mu (x,)←h_Modify1 (h_ND+f ((⇔) p)) s_0;η (x,s_0)1.5mu}[E]

[33](y,s_2)←𝐝𝐨 {1.5mu (y,)←h_Modify1 (h_ND+f ((⇔) q)) s_1;η (x,s_1)1.5mu}[E]

[33]Var (x++y,s_2)))[E]

[5]fmap (fmap fst) (λs_0→(𝐝𝐨 [33]
[33](x,)←h_Modify1 (h_ND+f ((⇔) p)) s_0[E]

[33](y,)←h_Modify1 (h_ND+f ((⇔) q)) s_0[E]

[33]Var (x++y,s_0)))[E]

[5]λs_0→(𝐝𝐨 [16]
[16](x,)←h_Modify1 (h_ND+f ((⇔) p)) s_0[E]

[16](y,)←h_Modify1 (h_ND+f ((⇔) q)) s_0[E]

[16]Var (x++y))[E]

[5]λs_0→(𝐝𝐨 [16]
[16]x←fmap fst (h_Modify1 (h_ND+f ((⇔) p)) s_0)[E]

[16]y←fmap fst (h_Modify1 (h_ND+f ((⇔) q)) s_0)[E]

[16]Var (x++y))[E]

[5]λs_0→(𝐝𝐨 [16]
[16]x←fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) p))) s_0[E]

[16]y←fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) q))) s_0[E]

[16]Var (x++y))[E]

[5]λs_0→(𝐝𝐨 [16]
[16]x←h_GlobalM p s_0[E]

[16]y←h_GlobalM q s_0[E]

[16]Var (x++y))[E]

[5]λs_0→liftM2 (++) (h_GlobalM p s_0) (h_GlobalM q s_0)[E]

[5]alg_LHS^ND (Or (h_GlobalM p) (h_GlobalM q))[E]

[5]alg_LHS^ND (fmap hGobal (Or p q))[E]
For the last subcondition , we can define  as follows.B@>l<@
[3]fwd_LHS::Functor f⇒f (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]fwd_LHS op=λs→Op (fmap ($s) op)[E]
We prove it by the following calculation for input .

[5]h_GlobalM (alg (Inr (Inr op)))[E]

[5]h_GlobalM (Op (Inr (Inr op)))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inr op))))))[E]

[5]fmap (fmap fst) (h_Modify1 (h_ND+f (Op (Inr (Inr (fmap (⇔) op))))))[E]

[5]fmap (fmap fst) (h_Modify1 (Op (fmap h_ND+f (Inr (fmap (⇔) op)))))[E]

[5]fmap (fmap fst) (h_Modify1 (Op (Inr (fmap h_ND+f (fmap (⇔) op)))))[E]

[5]fmap (fmap fst) (h_Modify1 (Op (Inr (fmap (h_ND+f∘.(⇔)) op))))[E]

[5]fmap (fmap fst) (λs→Op (fmap ($s) (fmap h_Modify1 (fmap (h_ND+f∘.(⇔)) op))))[E]

[5]fmap (fmap fst) (λs→Op (fmap ($s) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op)))[E]

[5]λs→fmap fst (Op (fmap ($s) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op)))[E]

[5]λs→Op (fmap (fmap fst) (fmap ($s) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op)))[E]

[5]λs→Op (fmap (fmap fst∘.($s)) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op)))[E]

[5]λs→Op (fmap (($s)∘.fmap (fmap fst)) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op)))[E]

[5]λs→Op ((fmap ($s)∘.fmap (fmap (fmap fst))) (fmap (h_Modify1∘.h_ND+f∘.(⇔)) op))[E]

[5]λs→Op (fmap ($s) (fmap (fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)) op))[E]

[5]λs→Op (fmap ($s) (fmap h_GlobalM op))[E]

[5]fwd_LHS (fmap h_GlobalM op)[E]

§.§ Equating the Fused Sides

We observe that the following equations hold trivially.

\begin{eqnarray*}
\ensuremath{\Varid{gen}_{\Varid{LHS}}} & = & \ensuremath{\Varid{gen}_{\Varid{RHS}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}} \\
\ensuremath{\Varid{fwd}_{\Varid{LHS}}} & = & \ensuremath{\Varid{fwd}_{\Varid{RHS}}}
\end{eqnarray*}

Therefore, the main theorem (<Ref>) holds.

§.§ Key Lemma: State Restoration

Similar to <Ref>, we have a key lemma saying that
restores the initial state after a computation.

For any program  that do
not use the operation , we have

\[\ba{ll}
&\ensuremath{\Varid{h_{Modify1}}\;(\Varid{h_{ND+f}}\;(\Varid{(\Leftrightarrow)}\;(\Varid{local2global_M}\;\Varid{p})))\;\Varid{s}} \\
= &\ensuremath{\mathbf{do}\;(\Varid{x},\anonymous )\leftarrow \Varid{h_{Modify1}}\;(\Varid{h_{ND+f}}\;(\Varid{(\Leftrightarrow)}\;(\Varid{local2global_M}\;\Varid{p})))\;\Varid{s};\Varid{\eta}\;(\Varid{x},\Varid{s})}
\ea\]

The proof follows the same structure of <Ref>.
We proceed by induction on .

[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Var y)))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) (Var y))) s[E]

[6]h_Modify1 (h_ND+f (Var y)) s[E]

[6]h_Modify1 (Var [1.5mu y1.5mu]) s[E]

[6]Var ([1.5mu y1.5mu],s)[E]

[6]𝐝𝐨 (x,)←Var ([1.5mu y1.5mu],s);Var (x,s)[E]

[6]𝐝𝐨 (x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M (Var y)))) s;η (x,s)[E]
[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inl (MGet k)))))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) (Op (Inl (MGet (local2global_M∘.k)))))) s[E]

[6]h_Modify1 (h_ND+f (Op (Inr (Inl (MGet ((⇔)∘.local2global_M∘.k)))))) s[E]

[6]h_Modify1 (Op (Inl (MGet (h_ND+f∘.(⇔)∘.local2global_M∘.k)))) s[E]

[6](h_Modify1∘.h_ND+f∘.(⇔)∘.local2global_M∘.k) s s[E]

[6](h_Modify1 (h_ND+f ((⇔) (local2global_M (k s))))) s[E]

[6]𝐝𝐨 (x,)←h_Modify1 ((⇔) (h_ND+f (local2global_M (k s)))) s;η (x,s)[E]

[6]𝐝𝐨 (x,)←h_Modify1 (h_ND+f (local2global_M (Op (Inl (MGet k))))) s;η (x,s)[E]
[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inl Fail)))))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inl Fail))))) s[E]

[6]h_Modify1 (h_ND+f (Op (Inl Fail))) s[E]

[6]h_Modify1 (Var [1.5mu 1.5mu]) s[E]

[6]Var ([1.5mu 1.5mu],s)[E]

[6]𝐝𝐨 (x,)←Var ([1.5mu 1.5mu],s);Var (x,s)[E]

[6]𝐝𝐨 (x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inl Fail)))))) s;η (x,s)[E]
[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inl (Put t k)))))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) ((update rside (restore r))>>local2global_M k))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) ([E]

[8]Op (Inr (Inl (Or [26]
[26](Op (Inl (MUpdate r (local2global_M k)))) [E]

[26](Op (Inl (MRestore r (Op (Inr (Inl Fail)))))))))))) s[E]

[6]h_Modify1 (h_ND+f ([E]

[8]Op (Inl (Or [21]
[21](Op (Inr (Inl (MUpdate r ((⇔) (local2global_M k)))))) [E]

[21](Op (Inr (Inl (MRestore r (Op (Inl Fail)))))))))) s[E]

[6]h_Modify1 ([E]

[8]liftM2 (++) [21]
[21](Op (Inl (MUpdate r (h_ND+f ((⇔) (local2global_M k)))))) [E]

[21](Op (Inl (MRestore r (Var [1.5mu 1.5mu]))))) s[E]

[6]h_Modify1 [16]
[16](𝐝𝐨 [21]
[21]x←Op (Inl (MUpdate r (h_ND+f ((⇔) (local2global_M k)))))[E]

[21]y←Op (Inl (MRestore r (Var [1.5mu 1.5mu])))[E]

[21]Var (x++y)[E]

[15]) s[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←h_Modify1 (Op (Inl (MUpdate r (h_ND+f ((⇔) (local2global_M k)))))) s[E]

[10](y,s_2)←h_Modify1 (Op (Inl (MRestore r (Var [1.5mu 1.5mu])))) s_1[E]

[10]Var (x++y,s_2)[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r)[E]

[10](y,s_2)←Var ([1.5mu 1.5mu],s_1⊖r)[E]

[10]Var (x++y,s_2)[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r)[E]

[10]Var (x++[1.5mu 1.5mu],s_1⊖r)[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r)[E]

[10]Var (x,s_1⊖r)[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←𝐝𝐨 {1.5mu (x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r);η (x,s⊕r)1.5mu}[E]

[10]Var (x,s_1⊖r)[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r)[E]

[10]Var (x,(s⊕r)⊖r)[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r)[E]

[10]Var (x,s)[E]

[6]𝐝𝐨 [10]
[10](x,)←𝐝𝐨 {1.5mu (x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M k))) (s⊕r);η (x,s)1.5mu}[E]

[10]Var (x,s)[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inl (MUpdate r k)))))) s[E]

[10]Var (x,s)[E]
[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inl (Or p q))))))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inl (Or (local2global_M p) (local2global_M q))))))) s[E]

[6]h_Modify1 (h_ND+f (Op (Inl (Or ((⇔) (local2global_M p)) ((⇔) (local2global_M q)))))) s[E]

[6]h_Modify1 (liftM2 (++) (h_ND+f ((⇔) (local2global_M p))) (h_ND+f ((⇔) (local2global_M q)))) s[E]

[6]h_Modify1 (𝐝𝐨 [20]
[20]x←h_ND+f ((⇔) (local2global_M p))[E]

[20]y←h_ND+f ((⇔) (local2global_M q))[E]

[20]Var (x++y)[E]

[14]) s[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←h_Modify1 (h_ND+f ((⇔) (local2global_M p))) s[E]

[10](y,s_2)←h_Modify1 (h_ND+f ((⇔) (local2global_M q))) s_1[E]

[10]h_Modify1 (Var (x++y)) s_2[E]

[6]𝐝𝐨 [10]
[10](x,s_1)←𝐝𝐨 {1.5mu (x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M p))) s;η (x,s)1.5mu}[E]

[10](y,s_2)←𝐝𝐨 {1.5mu (y,)←h_Modify1 (h_ND+f ((⇔) (local2global_M q))) s_1;η (y,s_1)1.5mu}[E]

[10]h_Modify1 (Var (x++y)) s_2[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M p))) s[E]

[10](y,)←h_Modify1 (h_ND+f ((⇔) (local2global_M q))) s_1[E]

[10]h_Modify1 (Var (x++y)) s[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M p))) s[E]

[10](y,)←h_Modify1 (h_ND+f ((⇔) (local2global_M q))) s[E]

[10]η (x++y,s)[E]

[6]𝐝𝐨 [10]

[12]𝐝𝐨 [16]
[16](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M p))) s[E]

[16](y,)←h_Modify1 (h_ND+f ((⇔) (local2global_M q))) s_1[E]

[16]η (x++y,s)[E]

[10]η (x,s)[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inl (Or p q))))))) s[E]

[10]η (x,s)[E]

[6]h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inr y)))))) s[E]

[6]h_Modify1 (h_ND+f ((⇔) (Op (Inr (Inr (fmap local2global_M y)))))) s[E]

[6]h_Modify1 (h_ND+f (Op (Inr (Inr (fmap ((⇔)∘.local2global_M) y))))) s[E]

[6]h_Modify1 (Op (Inr (fmap (h_ND+f∘.(⇔)∘.local2global_M) y))) s[E]

[6]Op (fmap (($s)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.local2global_M) y)[E]

[6]Op (fmap ((>>=λ(x,)→η (x,s))∘.($s)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.local2global_M) y)[E]

[6]𝐝𝐨 [10]
[10](x,)←Op (fmap (($s)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.local2global_M) y)[E]

[10]η (x,s)[E]

[6]𝐝𝐨 [10]
[10](x,)←h_Modify1 (h_ND+f ((⇔) (local2global_M (Op (Inr (Inr y)))))) s[E]

[10]η (x,s)[E]

§.§ Auxiliary Lemmas

The derivations above made use of several auxliary lemmas.
We prove them here.

\[
\ensuremath{\Varid{h_{Modify1}}\;(\Varid{p}>\!\!>\!\!=\Varid{k})\;\Varid{s}} \quad =\quad \ensuremath{\Varid{h_{Modify1}}\;\Varid{p}\;\Varid{s}>\!\!>\!\!=\lambda (\Varid{x},\Varid{s'})\to \Varid{h_{Modify1}}\;(\Varid{k}\;\Varid{x})\;\Varid{s'}}
\]

The proof follows the same structure of <Ref>.
We proceed by induction on .

[6]h_Modify1 (Var x>>=k) s[E]

[6]h_Modify1 (k x) s[E]

[6]η (x,s)>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Var x) s>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MGet p))>>=k) s[E]

[6]h_Modify1 (Op (fmap (>>=k) (Inl (MGet p)))) s[E]

[6]h_Modify1 (Op (Inl (fmap (>>=k) (MGet p)))) s[E]

[6]h_Modify1 (Op (Inl (MGet (λx→p s>>=k)))) s[E]

[6]h_Modify1 (p s>>=k) s[E]

[6]h_Modify1 (p s) s>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MGet p))) s>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MUpdate r p))>>=k) s[E]

[6]h_Modify1 (Op (fmap (>>=k) (Inl (MUpdate r p)))) s[E]

[6]h_Modify1 (Op (Inl (fmap (>>=k) (MUpdate r p)))) s[E]

[6]h_Modify1 (Op (Inl (MUpdate r (p>>=k)))) s[E]

[6]h_Modify1 (p>>=k) (s⊕r)[E]

[6]h_Modify1 p (s⊕r)>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MUpdate r p))) s>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MRestore r p))>>=k) s[E]

[6]h_Modify1 (Op (fmap (>>=k) (Inl (MRestore r p)))) s[E]

[6]h_Modify1 (Op (Inl (fmap (>>=k) (MRestore r p)))) s[E]

[6]h_Modify1 (Op (Inl (MRestore r (p>>=k)))) s[E]

[6]h_Modify1 (p>>=k) (s⊖r)[E]

[6]h_Modify1 p (s⊖r)>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inl (MRestore r p))) s>>=λ(x,s')→h_Modify1 (k x) s'[E]

[6]h_Modify1 (Op (Inr y)>>=k) s[E]

[6]h_Modify1 (Op (fmap (>>=k) (Inr y))) s[E]

[6]h_Modify1 (Op (Inr (fmap (>>=k) y))) s[E]

[6]Op (fmap (λx→h_Modify1 x s) (fmap (>>=k) y))[E]

[6]Op (fmap ((λx→h_Modify1 (x>>=k) s)) y)[E]

[6]Op (fmap (λx→h_Modify1 x s>>=λ(x',s')→h_Modify1 (k x') s') y)[E]

[6]Op (fmap (λx→x>>=λ(x',s')→h_Modify1 (k x') s') (fmap (λx→h_Modify1 x s) y))[E]

[6]Op ((fmap (λx→h_Modify1 x s) y))>>=λ(x',s')→h_Modify1 (k x') s'[E]

[6]Op (Inr y) s>>=λ(x',s')→h_Modify1 (k x') s'[E]

§ PROOFS FOR MODELLING LOCAL STATE WITH TRAIL STACK

In this section, we prove the following theorem in

The proof follows a similar structure to those in
<Ref> and <Ref>.

As in <Ref>, we fuse
into  and use it instead in the following proofs.

§.§ Main Proof Structure

The main proof structure of <Ref> is as follows.

The left-hand side is expanded to
[3]h_GlobalT=fmap (fmap fst∘.flip run_StateT (Stack [1.5mu 1.5mu])∘.h_State)∘.h_GlobalM∘.local2trail[E]
Both the left-hand side and the right-hand side of the equation
consist of function compositions involving one or more folds.
We apply fold fusion separately on both sides to contract each
into a single fold:

\begin{eqnarray*}
\ensuremath{\Varid{h_{GlobalT}}} & = & \ensuremath{\Varid{fold}\;\Varid{gen}_{\Varid{LHS}}\;(\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{LHS}})} \\
\ensuremath{\Varid{h_{LocalM}}}& = & \ensuremath{\Varid{fold}\;\Varid{gen}_{\Varid{RHS}}\;(\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{RHS}})}
\end{eqnarray*}

Finally, we show that both folds are equal by showing that their
corresponding parameters are equal:

\begin{eqnarray*}
\ensuremath{\Varid{gen}_{\Varid{LHS}}} & = & \ensuremath{\Varid{gen}_{\Varid{RHS}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}} \\
\ensuremath{\Varid{fwd}_{\Varid{LHS}}} & = & \ensuremath{\Varid{fwd}_{\Varid{RHS}}}
\end{eqnarray*}

We elaborate each of these steps below.

§.§ Fusing the Right-Hand Side

We have already fused  in <Ref>.
We just show the result here for easy reference.
[B]h_LocalM=fold gen_RHS (alg_RHS^S#alg_RHS^ND#fwd_RHS)[E]

[5]gen_RHS::Functor f⇒a→(s→Free f [1.5mu a1.5mu])[E]

[5]gen_RHS x=λs→Var [1.5mu x1.5mu][E]

[5]alg_RHS^S::Undo s r⇒State_F s (s→p)→(s→p)[E]

[5]alg_RHS^S (MGet k)[29]
[29]=λs→k s s[E]

[5]alg_RHS^S (MUpdate r k)[29]
[29]=λs→k (s⊕r)[E]

[5]alg_RHS^S (MRestore r k)[29]
[29]=λs→k (s⊕r)[E]

[5]alg_RHS^ND::Functor f⇒Nondet_F (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[5]alg_RHS^ND Fail[24]
[24]=λs→Var [1.5mu 1.5mu][E]

[5]alg_RHS^ND (Or p q)[24]
[24]=λs→liftM2 (++) (p s) (q s)[E]

[5]fwd_RHS::Functor f⇒f (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[5]fwd_RHS op=λs→Op (fmap ($s) op)[E]

§.§ Fusing the Left-Hand Side

As in <Ref>, we fuse
into .
For brevity, we defineB@>l<@
[3]runStack=fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])[E]

The left-hand side is simplified toB@>l<@
[3]fmap runStack∘.h_GlobalM∘.local2trail[E]
We calculate as follows:
[5]fmap runStack∘.h_GlobalM∘.local2trail[E]

[5]fmap runStack∘.h_GlobalM∘.fold Var (alg_1#alg_2#fwd)[E]

[9]alg_1 (MUpdate r k)[29]
[29]=pushStack (Left r)>>update r>>k[E]

[9]alg_1 p[29]

[9]alg_2 (Or p q)[29]
[29]=(pushStack (Right ())>>p)(untrail>>q)[E]

[9]alg_2 p[29]

[9]fwd p[29]

[9]untrail=𝐝𝐨 [25]

[25]𝐜𝐚𝐬𝐞 top 𝐨𝐟[E]

[27]Nothing→η ()[E]

[27]Just (Right ())→η ()[E]

[27]Just (Left r)→𝐝𝐨 restore r;untrail[E]

[5]fold gen_LHS (alg_LHS^S#alg_LHS^ND#fwd_LHS)[E]
This last step is valid provided that the fusion conditions are satisfied:

\[\ba{rclr}
\ensuremath{\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Conid{Var}} & = & \ensuremath{\Varid{gen}_{\Varid{LHS}}} &\refa{}\\
\ea\]

\[\ba{rlr}
&\ensuremath{\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}(\Varid{alg}_{1}\mathbin{\#}\Varid{alg}_{2}\mathbin{\#}\Varid{fwd})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} \\
= & \ensuremath{(\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\mathbin{\#}\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}\mathbin{\#}\Varid{fwd}_{\Varid{LHS}})\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} &\refb{}
\ea\]

The first subcondition  is met byB@>l<@
[3]gen_LHS::Functor f⇒a→(s→Free f [1.5mu a1.5mu])[E]

[3]gen_LHS x=λs→Var [1.5mu x1.5mu][E]
as established in the following calculation:B@>l<@
[5]fmap runStack$h_GlobalM (Var x)[E]

[5]fmap runStack$fmap (fmap fst) (h_Modify1 (h_ND+f ((⇔) (Var x))))[E]

[5]fmap runStack$fmap (fmap fst) (h_Modify1 (h_ND+f (Var x)))[E]

[5]fmap runStack$fmap (fmap fst) (h_Modify1 (Var [1.5mu x1.5mu]))[E]

[5]fmap runStack$fmap (fmap fst) (λs→Var ([1.5mu x1.5mu],s))[E]

[5]fmap runStack$λs→Var [1.5mu x1.5mu][E]

[5]λs→runStack$Var [1.5mu x1.5mu][E]

[5]λs→fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])$Var [1.5mu x1.5mu][E]

[5]λs→fmap fst$(λs→Var ([1.5mu x1.5mu],s)) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst (Var ([1.5mu x1.5mu],Stack [1.5mu 1.5mu]))[E]

[5]λs→Var [1.5mu x1.5mu][E]

[5]gen_LHS x[E]
We can split the second fusion condition  in three

\[\ba{rlr}
& \ensuremath{\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}_{1}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} \\
= & \ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} &\refc{}\\
& \ensuremath{\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{alg}_{2}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} \\
= & \ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} &\refd{}\\
& \ensuremath{\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{h_{GlobalM}}\hsdot{\circ }{.}\Varid{fwd}\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} \\
= & \ensuremath{\Varid{fwd}_{\Varid{LHS}}\hsdot{\circ }{.}\Varid{fmap}\;(\Varid{fmap}\;\Varid{runStack}\hsdot{\circ }{.}\Varid{h_{GlobalM}})\hsdot{\circ }{.}\Varid{fmap}\;\Varid{local2trail}} &\refe{}
\ea\]

For brevity, we omit the last common part  of
these equations. Instead, we assume that the input is in the codomain
of .

For the first subcondition , we define  as follows.B@>l<@
[3]alg_LHS^S::(Functor f,Undo s r)⇒Modify_F s r (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]alg_LHS^S (MGet k)[27]
[27]=λs→k s s[E]

[3]alg_LHS^S (MUpdate r k)[27]
[27]=λs→k (s⊕r)[E]

[3]alg_LHS^S (MRestore r k)[27]
[27]=λs→k (s⊖r)[E]
We prove it by a case analysis on the shape of input .
We use the condition in <Ref> that the input
program does not use the  operation.
We only need to consider the case that  is of form  or
where  is also not used in the continuation

In the corresponding case of <Ref>, we have
calculated that  .
[5]fmap runStack$h_GlobalM (alg_1 (MGet k))[E]

[5]fmap runStack$h_GlobalM (Op (Inl (MGet k)))[E]

[5]fmap runStack$λs→(h_GlobalM∘.k) s s[E]

[5]λs→runStack$(h_GlobalM∘.k) s s[E]

[5]λs→(fmap runStack∘.h_GlobalM∘.k) s s[E]

[5]alg_LHS^S (MGet (fmap runStack∘.h_GlobalM∘.k))[E]

[5]alg_LHS^S (fmap (fmap runStack∘.h_GlobalM) (MGet k))[E]

From  is in the codomain of  we obtain  is
in the codomain of .
[5]fmap runStack∘.h_GlobalM$alg_1 (MUpdate r k)[E]

[5]fmap runStack∘.h_GlobalM$pushStack (Left r)>>update r>>k[E]

[5]fmap runStack∘.h_GlobalM$𝐝𝐨[E]

[7]Stack xs←get[E]

[7]put (Stack (Left r:xs))[E]

[7]update r>>k[E]

[5]fmap runStack∘.h_GlobalM$[E]

[7]Op∘.Inr∘.Inr∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inr∘.Inr∘.Inl$Put (Stack (Left r:xs)) ([E]

[11]Op∘.Inl$MUpdate r k))[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)$[E]

[7]Op∘.Inr∘.Inr∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inr∘.Inr∘.Inl$Put (Stack (Left r:xs)) ([E]

[11]Op∘.Inl$MUpdate r k))[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1∘.h_ND+f$[E]

[7]Op∘.Inr∘.Inr∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inr∘.Inr∘.Inl$Put (Stack (Left r:xs)) ([E]

[11]Op∘.Inr∘.Inl$MUpdate r ((⇔) k)))[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1$[E]

[7]Op∘.Inr∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inr∘.Inl$Put (Stack (Left r:xs)) ([E]

[11]Op∘.Inl$MUpdate r (h_ND+f∘.(⇔)$k)))[E]

[5]fmap runStack∘.fmap (fmap fst)$λs→[E]

[7]Op∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inl$Put (Stack (Left r:xs)) ([E]

[11](h_Modify1∘.h_ND+f∘.(⇔)$k) (s⊕r)))[E]

[5]fmap runStack$λs→[E]

[7]Op∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inl$Put (Stack (Left r:xs)) ([E]

[11](fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)$k) (s⊕r)))[E]

[7]Op∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inl$Put (Stack (Left r:xs)) ([E]

[11](fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)$k) (s⊕r)))[E]

[7]Op∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inl$Put (Stack (Left r:xs)) ([E]

[11](h_GlobalM k) (s⊕r)))[E]

[5]λs→fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])$[E]

[7]Op∘.Inl$Get (λ(Stack xs)→[E]

[9]Op∘.Inl$Put (Stack (Left r:xs)) ([E]

[11](h_GlobalM k) (s⊕r)))[E]

[5]λs→fmap fst$(λt→[E]

[7](λ(Stack xs)→λ→[E]

[9]((fmap h_State1∘.h_GlobalM$k) (s⊕r)) (Stack (Left r:xs))[E]

[7]) t t[E]

[5])(Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$[E]

[7](λ(Stack xs)→λ→[E]

[9]((fmap h_State1∘.h_GlobalM$k) (s⊕r)) (Stack (Left r:xs))[E]

[7]) (Stack [1.5mu 1.5mu]) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$[E]

[9]((fmap h_State1∘.h_GlobalM$k) (s⊕r)) (Stack (Left r:[1.5mu 1.5mu]))[E]

[7]) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$[E]

[7]((fmap h_State1∘.h_GlobalM$k) (s⊕r)) (Stack (Left r:[1.5mu 1.5mu]))[E]

[5]λs→fmap fst$[E]

[7]((fmap h_State1∘.h_GlobalM$k) (s⊕r)) (Stack (Left r:[1.5mu 1.5mu]))[E]

[5]λs→(fmap (fmap fst∘.flip h_State1 (Stack [1.5mu Left r1.5mu]))∘.h_GlobalM$k) (s⊕r)[E]

[5]λs→(fmap (fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu]))∘.h_GlobalM$k) (s⊕r)[E]

[5]λs→(fmap runStack∘.h_GlobalM$k) (s⊕r)[E]

[5]alg_LHS^S (MUpdate r (fmap runStack∘.h_GlobalM$k))[E]

[5]alg_LHS^S (fmap (fmap runStack∘.h_GlobalM) (MUpdate r k))[E]
For the second subcondition , we can define  as
[3]alg_LHS^ND::Functor f⇒Nondet_F (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]alg_LHS^ND Fail[22]
[22]=λs→Var [1.5mu 1.5mu][E]

[3]alg_LHS^ND (Or p q)[22]
[22]=λs→liftM2 (++) (p s) (q s)[E]
We prove it by a case analysis on the shape of input .

In the corresponding case of <Ref>, we have
calculated that  .
[5]fmap runStack$h_GlobalM (alg_2 (Fail))[E]

[5]fmap runStack$h_GlobalM (Op (Inr (Inl Fail)))[E]

[5]fmap runStack$λs→Var [1.5mu 1.5mu][E]

[5]λs→runStack$Var [1.5mu 1.5mu][E]

[5]λs→fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])$Var [1.5mu 1.5mu][E]

[5]λs→fmap fst$Var ([1.5mu 1.5mu],Stack [1.5mu 1.5mu])[E]

[5]λs→Var [1.5mu 1.5mu][E]

[4]alg_RHS^ND Fail[E]

[4]alg_RHS^ND (fmap (fmap runStack∘.h_GlobalM) Fail)[E]

From  is in the codomain of  we obtain  and
are in the codomain of .
[5]fmap runStack∘.h_GlobalM$alg_2 (Or p q)[E]

[5]fmap runStack∘.h_GlobalM$(pushStack (Right ())>>p)(untrail>>q)[E]

[5]fmap runStack∘.h_GlobalM$Op∘.Inr∘.Inl$Or[E]

[7](pushStack (Right ())>>p) (untrail>>q)[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1∘.h_ND+f∘.(⇔)$Op∘.Inr∘.Inl$Or[E]

[7](pushStack (Right ())>>p) (untrail>>q)[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1∘.h_ND+f$Op∘.Inl$Or[E]

[7](pushStack (Right ())>>(⇔) p) (untrail>>(⇔) q)[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1$𝐝𝐨[E]

[7]x←h_ND+f ((⇔) (pushStack (Right ())))>>h_ND+f ((⇔) p)[E]

[7]y←h_ND+f ((⇔) untrail)>>h_ND+f ((⇔) q)[E]

[7]η (x++y)[E]

[5]fmap runStack∘.fmap (fmap fst)∘.h_Modify1$𝐝𝐨[E]

[7]h_ND+f ((⇔) (pushStack (Right ())))[E]

[7]x←h_ND+f ((⇔) p)[E]

[7]h_ND+f ((⇔) untrail)[E]

[7]y←h_ND+f ((⇔) q)[E]

[7]η (x++y)[E]

[5]fmap runStack∘.fmap (fmap fst)$λs→𝐝𝐨[E]

[16]←h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s[E]

[16]←h_Modify1 (h_ND+f ((⇔) p)) s_1[E]

[16]←h_Modify1 (h_ND+f ((⇔) untrail)) s_2[E]

[16]←h_Modify1 (h_ND+f ((⇔) q)) s3[E]

[7]η (x++y,s4)[E]

[5]fmap runStack$λs→𝐝𝐨[E]

[7](,s_1)←h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s[E]

[7](x,s_2)←h_Modify1 (h_ND+f ((⇔) p)) s_1[E]

[7](,s3)←h_Modify1 (h_ND+f ((⇔) untrail)) s_2[E]

[12])←h_Modify1 (h_ND+f ((⇔) q)) s3[E]

[7]η (x++y)[E]

[5]λs→fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])$𝐝𝐨[E]

[7](,s_1)←h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s[E]

[7](x,s_2)←h_Modify1 (h_ND+f ((⇔) p)) s_1[E]

[7](,s3)←h_Modify1 (h_ND+f ((⇔) untrail)) s_2[E]

[12])←h_Modify1 (h_ND+f ((⇔) q)) s3[E]

[7]η (x++y)[E]

[5]λs→fmap fst$(λt→𝐝𝐨[E]

[7]((,s_1),t_1)←h_State1 (h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s) t[E]

[7]((x,s_2),t_2)←h_State1 (h_Modify1 (h_ND+f ((⇔) p)) s_1) t_1[E]

[7]((,s3),t3)←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[13]),t4)←h_State1 (h_Modify1 (h_ND+f ((⇔) q)) s3) t3[E]

[7]η (x++y,t4)) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$𝐝𝐨[E]

[7]((,s_1),t_1)←h_State1 (h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s) (Stack [1.5mu 1.5mu])[E]

[7]((x,s_2),t_2)←h_State1 (h_Modify1 (h_ND+f ((⇔) p)) s_1) t_1[E]

[7]((,s3),t3)←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[13]),t4)←h_State1 (h_Modify1 (h_ND+f ((⇔) q)) s3) t3[E]

[7]η (x++y,t4)[E]

[7]((,s_1),t_1)←h_State1 (h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s) (Stack [1.5mu 1.5mu])[E]

[7]((x,s_2),t_2)←h_State1 (h_Modify1 (h_ND+f ((⇔) p)) s_1) t_1[E]

[7]((,s3),t3)←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[18])←h_State1 (h_Modify1 (h_ND+f ((⇔) q)) s3) t3[E]

[7]η (x++y)[E]

[18])←h_State1 (h_Modify1 (h_ND+f ((⇔) p)) s) (Stack [1.5mu 1.5mu])[E]

[18])←h_State1 (h_Modify1 (h_ND+f ((⇔) q)) s) (Stack [1.5mu 1.5mu])[E]

[7]η (x++y)[E]

[7](x,)←runStack (h_Modify1 (h_ND+f ((⇔) p)) s)[E]

[7](y,)←runStack (h_Modify1 (h_ND+f ((⇔) q)) s)[E]

[7]η (x++y)[E]

[7]x←runStack (h_GlobalM p s)[E]

[7]y←runStack (h_GlobalM q s)[E]

[7]η (x++y)[E]

[7]x←(fmap runStack∘.hGobalM) p s[E]

[7]y←(fmap runStack∘.hGobalM) q s[E]

[7]η (x++y))[E]

[5]λs→liftM2 (++) ((fmap runStack∘.hGobalM) p s) ((fmap runStack∘.hGobalM) q s)[E]

[5]alg_LHS^ND (Or ((fmap runStack∘.hGobalM) p) ((fmap runStack∘.hGobalM) q))[E]

[5]alg_LHS^ND (fmap (fmap runStack∘.hGobalM) (Or p q))[E]
For the last subcondition , we can define  as follows.B@>l<@
[3]fwd_LHS::Functor f⇒f (s→Free f [1.5mu a1.5mu])→(s→Free f [1.5mu a1.5mu])[E]

[3]fwd_LHS op=λs→Op (fmap ($s) op)[E]
We prove it by the following calculation for input .
In the corresponding case of <Ref>, we have
calculated that  .
[5]fmap runStack$h_GlobalM (fwd op)[E]

[5]fmap runStack$h_GlobalM (Op∘.Inr∘.Inr∘.Inr$op)[E]

[5]fmap runStack$λs→Op (fmap ($s) (fmap h_GlobalM (Inr op)))[E]

[5]fmap runStack$λs→Op (fmap (($s)∘.h_GlobalM) (Inr op))[E]

[5]fmap runStack$λs→Op (fmap (λx→h_GlobalM x s) (Inr op))[E]

[5]λs→runStack$Op (fmap (λx→h_GlobalM x s) (Inr op))[E]

[5]λs→fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu])$[E]

[7]Op (fmap (λx→h_GlobalM x s) (Inr op))[E]

[5]λs→fmap fst$(λt→[E]

[7]Op (fmap ($t)∘.fmap (h_State1)$fmap (λx→h_GlobalM x s) op)) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$(λt→[E]

[7]Op (fmap (λx→h_State1 (h_GlobalM x s) t) op)) (Stack [1.5mu 1.5mu])[E]

[5]λs→fmap fst$[E]

[7]Op (fmap (λx→h_State1 (h_GlobalM x s) (Stack [1.5mu 1.5mu])) op)[E]

[5]λs→Op (fmap (λx→fmap fst (h_State1 (h_GlobalM x s) (Stack [1.5mu 1.5mu]))) op)[E]

[5]λs→Op (fmap (λx→fmap (fmap fst∘.flip h_State1 (Stack [1.5mu 1.5mu]))∘.h_GlobalM$x s) op)[E]

[5]λs→Op (fmap (λx→(fmap runStack∘.h_GlobalM$x) s) op)[E]

[5]λs→Op (fmap ($s) (fmap (fmap runStack∘.h_GlobalM) op))[E]

[5]fwd_LHS (fmap (fmap runStack∘.h_GlobalM) op)[E]

§.§ Equating the Fused Sides

We observe that the following equations hold trivially.

\begin{eqnarray*}
\ensuremath{\Varid{gen}_{\Varid{LHS}}} & = & \ensuremath{\Varid{gen}_{\Varid{RHS}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{S}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{S}}} \\
\ensuremath{\Varid{alg}_{\Varid{LHS}}^{\Varid{ND}}} & = & \ensuremath{\Varid{alg}_{\Varid{RHS}}^{\Varid{ND}}} \\
\ensuremath{\Varid{fwd}_{\Varid{LHS}}} & = & \ensuremath{\Varid{fwd}_{\Varid{RHS}}}
\end{eqnarray*}

Therefore, the main theorem (<Ref>) holds.

§.§ Lemmas

In this section, we prove the lemmas used in <Ref>.

The following lemma shows the relationship between the state and trail
stack. Intuitively, the trail stack contains all the deltas (updates)
that have not been restored in the program. Previous elements in the
trail stack do not influence the result and state of programs.

For , , and  which does not use the  operation, we
[6]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) t[E]

[6]𝐝𝐨 [10]
[10]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[10]η ((x,fplus s ys),extend t ys)[E]

for some . The functions  and
are defined as follows:
[B]extend::Stack s→[1.5mu s1.5mu]→Stack s[E]

[B]extend (Stack xs) ys=Stack (ys++xs)[E]

[B]fplus::Undo s r⇒s→[1.5mu Either r b1.5mu]→s[E]

[B]fplus s ys=foldr (λ(Left r) s→s⊕r) s ys[E]

Note that an immediate corollary of
<Ref> is that in addition to replacing
the stack  with the empty stack , we can also replace it
with any other stack. The following equation holds.
[6]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) t[E]

[6]𝐝𝐨 [10]
[10]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) t'[E]

[10]η ((x,fplus s ys),extend t ys)[E]

We will also use this corollary in the proofs.

We proceed by induction on .

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Var y)) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Var y) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f) (Var y) s) t[E]

[5]h_State1 (h_Modify1 (Var [1.5mu y1.5mu]) s) t[E]

[5]h_State1 (Var ([1.5mu y1.5mu],s)) t[E]

[4]Var (([1.5mu y1.5mu],s),t)[E]

[4]𝐝𝐨 [8]
[8]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Var y)) s) (Stack [1.5mu 1.5mu])[E]

[8]Var ((x,s),t)[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op∘.Inr∘.Inl$Fail)) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Op∘.Inr∘.Inl$Fail) s) t[E]

[5]h_State1 (h_Modify1 (Var [1.5mu 1.5mu]) s) t[E]

[5]h_State1 (Var ([1.5mu 1.5mu],s)) t[E]

[4]Var (([1.5mu 1.5mu],s),t)[E]

[4]𝐝𝐨 [8]
[8]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[25](local2trail (Op∘.Inr∘.Inl$Fail)) s) (Stack [1.5mu 1.5mu])[E]

[8]Var ((x,s),t)[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op (Inl (MGet k)))) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Op (Inl (MGet (local2trail∘.k)))) s) t[E]

[5]h_State1 (h_Modify1 (Op (Inl (MGet (h_ND+f∘.(⇔)∘.local2trail∘.k)))) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail∘.k) s s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (k s)) s) t[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (k s)) s) (Stack [1.5mu 1.5mu])[E]

[9]η ((x,fplus s ys),extend t ys)[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[26](local2trail (Op (Inl (MGet k)))) s) (Stack [1.5mu 1.5mu])[E]

[9]η ((x,fplus s ys),extend t ys)[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op (Inl (MUpdate r k)))) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (𝐝𝐨[E]

[7]pushStack (Left r)[E]

[7]update r[E]

[7]local2trail k[E]

[5])s) t[E]

[5]h_State1 (h_Modify1 (𝐝𝐨[E]

[7]h_ND+f∘.(⇔)$pushStack (Left r)[E]

[7]h_ND+f∘.(⇔)$update r[E]

[5])s) t[E]

[5]h_State1 (𝐝𝐨[E]

[7](,s_1)←(h_Modify1∘.h_ND+f∘.(⇔)$pushStack (Left r)) s[E]

[7](,s_2)←(h_Modify1∘.h_ND+f∘.(⇔)$update r) s_1[E]

[7](h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail$k) s_2[E]

[5]) t[E]

[5]h_State1 (𝐝𝐨[E]

[7](,s_1)←(h_Modify1∘.h_ND+f∘.(⇔)$pushStack (Left r)) s[E]

[7](,s_2)←η ([1.5mu ()1.5mu],s_1⊕r)[E]

[7](h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail$k) s_2[E]

[5]) t[E]

[5]h_State1 (𝐝𝐨[E]

[7](,s_1)←(h_Modify1∘.h_ND+f∘.(⇔)$pushStack (Left r)) s[E]

[7](h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail$k) (s_1⊕r)[E]

[5]) t[E]

[5]𝐝𝐨 [9]
[9]((,s_1),t_1)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)$pushStack (Left r)) s) t[E]

[9]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail$k) (s_1⊕r)) t_1[E]

[5]𝐝𝐨 [9]
[9]((,s_1),t_1)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)$𝐝𝐨[E]

[11]Stack xs←get[E]

[11]put (Stack (Left r:xs))) s) t[E]

[9]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail$k) (s_1⊕r)) t_1[E]

[5]𝐝𝐨 [9]
[9]((,s_1),t_1)←η (([1.5mu ()1.5mu],s),Stack (Left r:xs))[E]

[9]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail k) (s_1⊕r)) t_1[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail k) (s⊕r)) (Stack (Left r:xs))[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[24](local2trail k) (s⊕r)) (Stack [1.5mu Left r1.5mu])[E]

[9]η ((x,fplus (s⊕r) ys),extend (Stack (Left r:xs)) ys)[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[24](local2trail k) (s⊕r)) (Stack [1.5mu Left r1.5mu])[E]

[9]η ((x,fplus s (ys++[1.5mu Left r1.5mu])),extend (Stack xs) (ys++[1.5mu Left r1.5mu]))[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[24](local2trail k) (s⊕r)) (Stack [1.5mu Left r1.5mu])[E]

[9]η ((x,fplus s ys'),extend t ys')[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[24](local2trail (Op (Inl (MUpdate r k)))) s) (Stack [1.5mu 1.5mu])[E]

[9]η ((x,fplus s ys'),extend t ys')[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op∘.Inr∘.Inl$Or p q)) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) ([E]

[7](pushStack (Right ())>>local2trail p)(untrail>>local2trail q)) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Op∘.Inr∘.Inl$Or[E]

[7](pushStack (Right ())>>local2trail p)[E]

[7](untrail>>local2trail q)) s) t[E]

[5]h_State1 (h_Modify1 (𝐝𝐨[E]

[7]x←h_ND+f ((⇔) (pushStack (Right ())))>>h_ND+f ((⇔) (local2trail p))[E]

[7]y←h_ND+f ((⇔) untrail)>>h_ND+f ((⇔) (local2trail q))[E]

[7]η (x++y)[E]

[5])s) t[E]

[5]h_State1 (h_Modify1 (𝐝𝐨[E]

[7]h_ND+f ((⇔) (pushStack (Right ())))[E]

[7]x←h_ND+f ((⇔) (local2trail p))[E]

[7]h_ND+f ((⇔) untrail)[E]

[7]y←h_ND+f ((⇔) (local2trail q))[E]

[7]η (x++y)[E]

[5])s) t[E]

[5]h_State1 (𝐝𝐨[E]

[16]←h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s[E]

[16]←h_Modify1 (h_ND+f ((⇔) (local2trail p))) s_1[E]

[16]←h_Modify1 (h_ND+f ((⇔) untrail)) s_2[E]

[16]←h_Modify1 (h_ND+f ((⇔) (local2trail q))) s3[E]

[7]η (x++y,s4)[E]

[5]) t[E]

[5]𝐝𝐨 [9]
[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (pushStack (Right ())))) s) t[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail p))) s_1) t_1[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail q))) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (𝐝𝐨[E]

[11]Stack xs←get[E]

[11]put (Stack (Right ():xs))))) s) t[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail p))) s_1) t_1[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail q))) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[24]←η (([1.5mu ()1.5mu],s),Stack (Right ():xs))[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail p))) s_1) t_1[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[24]←h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail q))) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 (h_Modify1 (h_ND+f ((⇔)[E]

[30](local2trail p))) s) (Stack (Right ():xs))[E]

[28]h_State1 (h_Modify1 (h_ND+f ((⇔) untrail)) s_2) t_2[E]

[28]h_State1 (h_Modify1 (h_ND+f ((⇔) (local2trail q))) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail p) s) (Stack (Right ():xs))[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail q) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail p) s) (Stack (Right ()))[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30]untrail (fplus s ys)) (extend (Stack (Right ():xs)) ys)[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail q) s3) t3[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail p) s) (Stack (Right ()))[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail q) (fminus (fplus s ys) ys)) (Stack xs)[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail p) s) (Stack (Right ()))[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail q) s) (Stack xs)[E]

[9]η ((x++y,s4),t4)[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail p) s) (Stack (Right ()))[E]

[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail q) s) (Stack [1.5mu 1.5mu])[E]

[9]η ((x++y,fplus s ys'),extend (Stack xs) ys')[E]

[5]𝐝𝐨 [9]
[28]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[30](local2trail (Op∘.Inr∘.Inl$Or p q)) s) (Stack [1.5mu 1.5mu])[E]

[9]η ((x,fplus s ys'),extend t ys')[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op∘.Inr∘.Inr$y)) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Op∘.Inr∘.Inr∘.Inr∘.fmap local2trail$y) s) t[E]

[5]h_State1 (h_Modify1 (Op∘.Inr∘.Inr∘.fmap (h_ND+f∘.(⇔)∘.local2trail)$y) s) t[E]

[5]h_State1 (Op∘.Inr∘.fmap (($s)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail)$y) t[E]

[5]Op∘.fmap (($t)∘.h_State1∘.($s)∘.h_Modify1∘.h_ND+f∘.(⇔)∘.local2trail)$y[E]

[5]Op∘.fmap (λk→h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail k) s) t)$y[E]

[5]Op∘.fmap (λk→𝐝𝐨[E]

[7]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail k) s) t[E]

[7]η ((x,fplus s ys),extend t ys))$y[E]

[5]𝐝𝐨 [9]
[9]((x,),)←Op∘.fmap (λk→[E]

[11]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail k) s) t)$y[E]

[9]η ((x,fplus s ys),extend t ys)[E]

[5]𝐝𝐨 [9]
[9]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail (Op∘.Inr∘.Inr$y)) s) t[E]

[9]η ((x,fplus s ys),extend t ys)[E]

The following lemma shows that the  function restores all
the updates in the trail stack until it reaches a time stamp .

For  and , we haveB@>l<@
[6]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s) t[E]

[6]η (([1.5mu ()1.5mu],fminus s ys),Stack xs)[E]
The function  is defined as follows:
[B]fminus::Undo s r⇒s→[1.5mu Either r b1.5mu]→s[E]

[B]fminus s ys=foldl (λs (Left r)→s⊖r) s ys[E]

We first calculate as follows:
[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (𝐝𝐨[E]

[7]𝐜𝐚𝐬𝐞 top 𝐨𝐟[E]

[9]Nothing→η ()[E]

[9]Just (Right ())→η ()[E]

[9]Just (Left r)→𝐝𝐨 restore r;untrail[E]

[5])s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (𝐝𝐨[E]

[7]top←𝐝𝐨 [18]
[18]Stack xs←get[E]

[18]𝐜𝐚𝐬𝐞 xs 𝐨𝐟[E]

[20][1.5mu 1.5mu][29]
[29]→η Nothing[E]

[29]→𝐝𝐨 put (Stack xs');η (Just x)[E]

[7]𝐜𝐚𝐬𝐞 top 𝐨𝐟[E]

[9]Nothing→η ()[E]

[9]Just (Right ())→η ()[E]

[9]Just (Left r)→𝐝𝐨 restore r;untrail[E]

[5])s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (𝐝𝐨[E]

[7]Stack xs←get[E]

[7]𝐜𝐚𝐬𝐞 xs 𝐨𝐟[E]

[9][1.5mu 1.5mu][27]
[27]→η ()[E]

[9](Right ():xs')[27]
[27]→𝐝𝐨 put (Stack xs');η ()[E]

[9](Left r[19]
[27]→𝐝𝐨 put (Stack xs');restore r;untrail[E]

[5])s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (Op∘.Inr∘.Inr∘.Inl∘.Get$λ(Stack xs)→[E]

[7]𝐜𝐚𝐬𝐞 xs 𝐨𝐟[E]

[9][1.5mu 1.5mu][27]
[27]→η ()[E]

[9](Right ():xs')[27]
[27]→𝐝𝐨 put (Stack xs');η ()[E]

[9](Left r[19]
[27]→𝐝𝐨 put (Stack xs');restore r;untrail[E]

[5])s) t[E]

[5]h_State1 (h_Modify1 (Op∘.Inr∘.Inl∘.Get$λ(Stack xs)→[E]

[7]𝐜𝐚𝐬𝐞 xs 𝐨𝐟[E]

[9][1.5mu 1.5mu][27]
[27]→η [1.5mu ()1.5mu][E]

[9](Right ():xs')[27]
[27]→h_ND+f∘.(⇔)$𝐝𝐨 put (Stack xs');η ()[E]

[9](Left r[19]
[27]→h_ND+f∘.(⇔)$𝐝𝐨 put (Stack xs');restore r;untrail[E]

[5])s) t[E]

[5]h_State1 (Op∘.Inl∘.Get$λ(Stack xs)→[E]

[7]𝐜𝐚𝐬𝐞 xs 𝐨𝐟[E]

[9][1.5mu 1.5mu][27]
[27]→η ([1.5mu ()1.5mu],s)[E]

[9](Right ():xs')[27]
[27]→h_Modify1 (h_ND+f∘.(⇔)$𝐝𝐨 put (Stack xs');η ()) s[E]

[9](Left r[19]
[27]→h_Modify1 (h_ND+f∘.(⇔)$𝐝𝐨 put (Stack xs');restore r;untrail) s[E]

[5]) t[E]

[7]𝐜𝐚𝐬𝐞 (ys++(Right ():xs)) 𝐨𝐟[E]

[9][1.5mu 1.5mu][27]
[27]→η (([1.5mu ()1.5mu],s),t)[E]

[9](Right ():xs')[27]
[27]→η (([1.5mu ()1.5mu],s),Stack xs')[E]

[9](Left r[19]
[27]→h_State1 (h_Modify1 (h_ND+f∘.(⇔)$[E]

[32]𝐝𝐨 put (Stack xs');restore r;untrail) s) t[E]
Then, we proceed by an induction on the structure of .

[5]𝐜𝐚𝐬𝐞 (ys++(Right ():xs)) 𝐨𝐟[E]

[7][1.5mu 1.5mu][25]
[25]→η (([1.5mu ()1.5mu],s),t)[E]

[7](Right ():xs')[25]
[25]→η (([1.5mu ()1.5mu],s),Stack xs')[E]

[7](Left r[17]
[25]→h_State1 (h_Modify1 (h_ND+f∘.(⇔)$[E]

[30]𝐝𝐨 put (Stack xs');restore r;untrail) s) t[E]

[5]η (([1.5mu ()1.5mu],s),Stack xs)[E]

[5]η (([1.5mu ()1.5mu],fminus s [1.5mu 1.5mu]),Stack xs)[E]
[5]𝐜𝐚𝐬𝐞 (ys++(Right ():xs)) 𝐨𝐟[E]

[7][1.5mu 1.5mu][25]
[25]→η (([1.5mu ()1.5mu],s),t)[E]

[7](Right ():xs')[25]
[25]→η (([1.5mu ()1.5mu],s),Stack xs')[E]

[7](Left r[17]
[25]→h_State1 (h_Modify1 (h_ND+f∘.(⇔)$[E]

[30]𝐝𝐨 put (Stack xs');restore r;untrail) s) t[E]

[5]h_State1 (h_Modify1 (h_ND+f∘.(⇔)$[E]

[7]𝐝𝐨 put (Stack (ys'++(Right ():xs)));restore r;untrail) s) t[E]

[5]h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail (s⊖r)) [E]

[7](Stack (ys'++(Right ():xs)))[E]

[5]η (([1.5mu ()1.5mu],fminus (s⊖r) ys'),Stack xs)[E]

[5]η (([1.5mu ()1.5mu],fminus s (Left r:ys')),Stack xs)[E]

[5]η (([1.5mu ()1.5mu],fminus s ys),Stack xs)[E]

The following lemma is obvious from
<Ref> and <Ref>.
It shows that we can restore the previous state and stack by pushing a
time stamp on the trail stack and use the function

For , , and  which does not use the  operation, we
[4]𝐝𝐨 [8]
[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (pushStack (Right ())) s) t[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s_1) t_1[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[8]η ((x,s),t)[E]

Suppose . We calculate as follows.
[4]𝐝𝐨 [8]
[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (pushStack (Right ())) s) (Stack xs)[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s_1) t_1[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[23]←η (([1.5mu ()1.5mu],s),Stack (Right ():xs))[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s_1) t_1[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) [E]

[28](Stack (Right ():xs))[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[23]←𝐝𝐨 [30]
[30]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[45](local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[30]η ((x,fplus s ys),extend (Stack (Right ():xs)) ys)[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) untrail s_2) t_2[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[8]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[23]←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔))[E]

[28]untrail (fplus s ys)) (Stack (ys++(Right ():xs)))[E]

[8]η ((x,s3),t3)[E]

[4]𝐝𝐨 [8]
[8]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[8]η ((x,fminus (fplus s ys) ys),Stack xs)[E]

[4]𝐝𝐨 [8]
[8]((x,),)←h_State1 ((h_Modify1∘.h_ND+f∘.(⇔)) (local2trail p) s) (Stack [1.5mu 1.5mu])[E]

[8]η ((x,s),Stack xs)[E]