fact: Definition JZ (X: counter) (p: nat) (offset: nat) : list mm_instr := concat ( let i := offset in [DEC X (JMP_len + 1 + i)] :: let i := 1 + i in JMP p :: let i := JMP_len + i in [INC X] :: []).
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun