proposition: Lemma MMA_mon_computable_iff {k} (R : Vector.t nat k -> nat -> Prop) : MMA_mon_computable R <-> (exists n : nat, exists P : list (mm_instr (Fin.t (S (k + n)))), Forall (fun instr => if instr is DEC c _ then NonZero c else True) P /\ (forall v m, R v m -> exists c v', (1, P) // (1, Vector.append (0 ## v) (Vector.const 0 n)) ~~> (c, m ## v')) /\ (forall v, sss.sss_terminates (@mma_sss _) (1, P) (1, Vector.append (0 ## v) (Vector.const 0 n)) -> exists m, R v m)).
proof: Proof. split. - move=> [n] [P] [H1P H2P]. exists n, P. split; [done|split]. + by move=> ?? /H2P. + move=> v [[c' v']]. rewrite (Vector.eta v') => HP. exists (Vector.hd v'). apply /H2P. do 2 eexists. eassumption. - move=> [n] [P] [H1P [H2P H3P]]. exists n, P. split; [done|split]. + apply: H2P. + move=> [c] [v'] Hm. have /H3P [m' Hm'] : sss_terminates (mma_sss (n:=S (k + n))) (1, P) (1, Vector.append (0 ## v) (Vector.const 0 n)). { eexists. eassumption. } suff : m' = m by move=> <-. move: Hm' Hm => /H2P [?] [?] /(sss_output_fun (@mma_sss_fun _)) /[apply]. by move=> /pair_equal_spec [_] /Vector.cons_inj []. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect