fact: Definition HALF (X: counter) (p: nat) (offset: nat) : list mm_instr := concat ( let i := offset in JMP (JMP_len + 1 + i) :: let i := JMP_len + i in let j := i in [INC A; DEC X (2+JMP_len+MOVE_len 1+i)] :: let i := 2 + i in MOVE A [X] i :: let i := MOVE_len 1 + i in JMP p :: let i := JMP_len + i in [DEC X j] :: let i := 1 + i in MOVE A [X] 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