proposition: Lemma halt_comp' (l : F1) (c : mconfig sig (state (projT1 (pM l))) n) : haltConf (M := StateWhileTM l) (lift c) = haltConf (M := projT1 (pM l)) c.
proof: Proof. cbn in *. destruct c as [q t]. cbn in *. unfold StateWhile_halt, haltConf. cbn. Abort. Lemma StateWhile_trans_repeat (l l_ : F1) (c : mconfig sig (state (projT1 (pM l))) n) (l' : F1) : haltConf (M := projT1 (pM l)) c = true -> projT2 (pM l) (cstate c) = inl l' -> step (StateWhileTM l_) (lift c) = lift (initc (projT1 (pM l')) (ctapes c)). Proof. intros HHalt HRepeat. unfold haltConf in HHalt. destruct c as [q t]; cbn in *. unfold step. cbn -[doAct_multi] in *. rewrite HHalt, HRepeat. unfold initc, lift. cbn. f_equal. apply doAct_nop. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts