proposition: Lemma exp_const i m : exp i (Vector.const 0 m) = 1.
proof: Proof. induction m in i |- *; cbn. - reflexivity. - now rewrite IHm. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss) Undecidability.FRACTRAN(FRACTRAN_computable mm_fractran prime_seq) Undecidability.Shared.Libs.DLW(gcd prime vec) Nat Arith Lia List