# Composed-shortcut-laws


fx.experimental.desc-interp.composed-shortcut-laws: six H.refl lemmas — state's three canonical ops on inl and error's three strategies on inr — anchoring `composedHandlerShortcut` soundness. Each chains `composeHandlersInl/InrLemma`, the per-effect uniform-shortcut lemma, and inner `sumElim` ι; all three reductions are conv-decidable.

## `errorCollectingInrLemma`

_H.refl proof of `errorCollectingInrLemmaTy`. Resume payload := `tt`; new s_B := `cons E payload s_B`._

## `errorCollectingInrLemmaTy`

_`Π E S_A A. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:List E. composeHandlers … H_A uniformOf_collecting (inr (error E payload)) (pair s_A s_B) ≡ mkResumeAt … tt (pair s_A (cons E payload s_B))`._

## `errorResultInrLemma`

_H.refl proof of `errorResultInrLemmaTy`. Abort channel `Sum E A_inner` carries `inl payload`._

## `errorResultInrLemmaTy`

_`Π E S_A S_B A_inner. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:S_B. composeHandlers … H_A uniformOf_result (inr (error E payload)) (pair s_A s_B) ≡ mkAbortAt … (Sum E A_inner) (inl E A_inner payload) (pair s_A s_B)`._

## `errorStrictInrLemma`

_H.refl proof of `errorStrictInrLemmaTy`. Strict always aborts; abort payload := `payload`._

## `errorStrictInrLemmaTy`

_`Π E S_A S_B. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:S_B. composeHandlers … H_A uniformOf_strict (inr (error E payload)) (pair s_A s_B) ≡ mkAbortAt … E payload (pair s_A s_B)`._

## `stateGetInlLemma`

_H.refl proof of `stateGetInlLemmaTy`. `handle_State (get S) s_A ι→ inl(pair s_A s_A)`; inner sumElim ι folds to the composed mkResumeAt._

## `stateGetInlLemmaTy`

_`Π E S_A A. Π H_B. Π s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (get S_A)) (pair s_A s_B) ≡ mkResumeAt … (inl (get S_A)) A s_A (pair s_A s_B)`._

## `stateModifyInlLemma`

_H.refl proof of `stateModifyInlLemmaTy`. New sub-state := `fn s_A`; resume payload := `tt`._

## `stateModifyInlLemmaTy`

_`Π E S_A A. Π H_B. Π fn:S_A→S_A. Π s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (modify S_A fn)) (pair s_A s_B) ≡ mkResumeAt … tt (pair (fn s_A) s_B)`._

## `statePutInlLemma`

_H.refl proof of `statePutInlLemmaTy`. New sub-state := `param`; resume payload := `tt`._

## `statePutInlLemmaTy`

_`Π E S_A A. Π H_B. Π param s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (put S_A param)) (pair s_A s_B) ≡ mkResumeAt … tt (pair param s_B)`._