proposition: Lemma exp_app {n} (v : Vector.t nat n) i m (w : Vector.t nat m) : exp i (Vector.append v w) = exp i v * exp (i + n) w.
proof: Proof. induction v in i, m, w |- *; cbn. - now rewrite !Nat.add_0_r. - rewrite IHv. ring_simplify. do 2 f_equal. lia. 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