let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i being No-StopCode Instruction of S st i is ins-loc-free holds
Macro i is closed
let i be No-StopCode Instruction of S; :: thesis: ( i is ins-loc-free implies Macro i is closed )
assume A1: i is ins-loc-free ; :: thesis: Macro i is closed
let i1 be Instruction of S; :: according to COMPOS_2:def 5 :: thesis: ( i1 in rng (Macro i) implies rng (JumpPart i1) c= dom (Macro i) )
assume i1 in rng (Macro i) ; :: thesis: rng (JumpPart i1) c= dom (Macro i)
then i1 in {i,(halt S)} by COMPOS_1:67;
then ( i1 = i or i1 = halt S ) by TARSKI:def 2;
then rng (JumpPart i1) = {} by A1;
hence rng (JumpPart i1) c= dom (Macro i) ; :: thesis: verum