fact: Definition PROG (offset : nat) : list mm_instr := concat ( let i := offset in JMP (JMP_len + i) :: let i := JMP_len + i in UNPACK U B i :: let i := UNPACK_len + i in [DEC B (CASE_VARS_len+CASE_VAR0_len+2+i)] :: let i := 1 + i in [DEC U (CASE_VAR0_len+1+i)] :: let i := 1 + i in CASE_VAR0 offset i :: let i := CASE_VAR0_len + i in CASE_VARS offset i :: let i := CASE_VARS_len + i in [DEC B (CASE_LAM_len+1+i)] :: let i := 1 + i in CASE_LAM offset i :: let i := CASE_LAM_len + i in CASE_APP offset 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