proposition: Theorem mma_mma0_sim_spec v : (i,P) //ₐ (i,v) ↓ <-> (1,R) //ₐ (1,v) ~~> (0,vec_zero).
proof: Proof. split. + intros ((i',v') & H). apply HQ in H; fold Q in H. destruct H as [ H _ ]. split; [ | simpl; lia ]. unfold R. apply subcode_sss_compute_trans with (2 := H); auto. apply subcode_sss_compute_trans with (2 := mma_null_all_spec _ _); auto. apply subcode_sss_compute with (2 := mma_jump_spec _ pos0 _ _); auto. + intros H. apply HQ; fold Q. apply subcode_sss_terminates with (Q := (1,R)). * unfold R; auto. * exists (0,vec_zero); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)