proposition: Lemma P'_mon : Forall (fun instr => if instr is DEC c _ then NonZero c else True) P'.
proof: Proof. rewrite /P'. apply /Forall_app. split. - apply /Forall_map /Forall_forall => - []; [done|]. move=> X ? _ /=. pattern X. apply: Fin.caseS'; [done|]. move=> {}X. rewrite /shift_counter /=. by case: (pos_both k k' X). - by do ? constructor. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect