proposition: Theorem mma_auto_simulator i (P : list (@mm_instr (pos n))) : { Q : list (@mm_instr (pos n)) | forall v, (forall i' v', (i,P) //ₐ (i,v) ~~> (i',v') -> (1,Q) //ₐ (1,v) ~~> (length Q+1,v')) /\ ((1,Q) //ₐ (1,v) ↓ -> (i,P) //ₐ (i,v) ↓) }.
proof: Proof. exists (gc_code mma_auto_compiler (i,P) 1). intros v; split. + intros i' v' H. apply (compiler_t_output_sound' mma_auto_compiler) with (i := 1) (w := v) in H as (w' & H1 & <-); eauto. rewrite Nat.add_comm; auto. + apply compiler_t_term_equiv; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)