proposition: Fact bsm_state_enc_spec v : v ⋈ bsm_state_enc v.
proof: Proof. red; unfold tmp1, tmp2; repeat split; rew vec. intros p; unfold reg; simpl. rewrite vec_pos_map; trivial. 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)