fact: Definition CASE_APP (p: nat) (offset : nat) : list mm_instr := concat ( let i := offset in PACK B CTX i :: let i := PACK_len + i in MOVE B [CTX; A] i :: let i := MOVE_len 2 + i in MOVE A [B] i :: let i := MOVE_len 1 + i in PACK TS CTX i :: let i := PACK_len + i in UNPACK B CTX i :: let i := UNPACK_len + i in ZERO B i :: let i := ZERO_len + i in JMP p :: []).
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