proposition: Lemma M_length : length M = a0+b0+b0+(length P * 6).
proof: Proof. rewrite /M !app_length !map_length !seq_length. suff: forall n, length (flat_map encode_instruction (combine P (seq n (length P)))) = length P * 6. { move=> ->. lia. } elim: (P). { done. } move=> > IH > /=. by rewrite app_length length_encode_instruction IH. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun