fact: Definition UNPACK (X Y: counter) (offset: nat) : list mm_instr := concat ( let i := offset in JZ X 0 i :: let i := JZ_len + i in ZERO A i :: let i := ZERO_len + i in ZERO Y i :: let i := ZERO_len + i in JMP (JMP_len + 1 + i) :: let j := JMP_len + i in [INC Y] :: let i := 1 + j in HALF X j i :: []).
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