proposition: Theorem bsm_mm_compiler_strong n i (P : list (bsm_instr n)) (tmp1 tmp2 tmp3 : pos (n + 3)) (reg : pos n -> pos (n + 3)) iQ : tmp1 <> tmp2 -> (forall p, tmp1 <> reg p) -> (forall p, tmp2 <> reg p) -> (forall p q, reg p = reg q -> p = q) -> tmp1 <> tmp3 -> tmp2 <> tmp3 -> (forall p, tmp3 <> reg p) -> forall cases : (forall p : pos _, {p = tmp1} + {p = tmp2} + {p = tmp3} + {q | p = reg q}), { Q : list (mm_instr (pos (n+3))) | (forall v, (i,P) /BSM/ (i,v) ↓ <-> (iQ,Q) /MM/ (iQ,(@vec_enc _ tmp1 tmp2 tmp3 reg cases v)) ↓) /\ forall v j w, (i,P) /BSM/ (i,v) ~~> (j,w) -> (iQ,Q) /MM/ (iQ, @vec_enc _ tmp1 tmp2 tmp3 reg cases v) ~~> (iQ + length Q, @vec_enc _ tmp1 tmp2 tmp3 reg cases w) }.
proof: Proof. intros. destruct bsm_mm_simulator with (tmp1 := tmp1) (tmp2 := tmp2) (tmp3 := tmp3) (reg := reg) (i := i) (P := P) (j := iQ) as (Q & HQ); auto. exists Q; split. + intros v; split. * intros ((j,w) & Hw). apply (HQ v (vec_enc _ cases v)) in Hw as (w' & Hw' & _). 2: apply vec_enc_spec; auto. now exists (iQ+length Q,w'). * apply HQ, vec_enc_spec; auto. + intros v j w G. destruct (HQ v (vec_enc _ cases v)) as [ HQ' _ ]. 1: apply vec_enc_spec; auto. destruct HQ' with (1 := G) as (w' & Hw1 & Hw2). assert (vec_enc _ cases w = w') as ->; auto. apply bsm_state_enc_fun with (3 := Hw2); auto. apply vec_enc_spec; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)