proposition: Lemma length_encode_instruction instr i : length (encode_instruction (instr, i)) = 6.
proof: Proof. by case: instr. 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