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

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