fact: Definition M : list CM1.Instruction := map (fun i => (1+i, 0)) (seq 0 (a0+b0)) ++ map (fun i => (1+i, 1)) (seq (a0+b0) (b0)) ++ flat_map encode_instruction (combine P (seq 1 (length P))).
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