proposition: Theorem eval_iff n i (P : list (mm_instr (pos n))) c (v : vec nat n) c' v' : eval (i, P) (c, v) (c', v') <-> sss_output (@mm_sss _) (i,P) (c, v) (c', v').
proof: Proof. split. - intros H. split. + now eapply eval_to_sss_compute. + eapply eval_to_sss_out_code. eassumption. - intros H. now eapply sss_output_to_eval. Qed.
imports: Coq(List Lia) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM