let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for i being Instruction of S holds
( (Macro i) . 0 = i & (Macro i) . 1 = halt S & (Initialize (Macro i)) . 0 = i )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for i being Instruction of S holds
( (Macro i) . 0 = i & (Macro i) . 1 = halt S & (Initialize (Macro i)) . 0 = i )
let i be Instruction of S; :: thesis: ( (Macro i) . 0 = i & (Macro i) . 1 = halt S & (Initialize (Macro i)) . 0 = i )
thus A1: (Macro i) . 0 = i by FUNCT_4:66; :: thesis: ( (Macro i) . 1 = halt S & (Initialize (Macro i)) . 0 = i )
thus (Macro i) . 1 = halt S by FUNCT_4:66; :: thesis: (Initialize (Macro i)) . 0 = i
A2: 0 in dom (Macro i) by Th147;
dom (Macro i) misses dom (Start-At (0,S)) by Th140;
then Macro i c= Initialize (Macro i) by FUNCT_4:33;
hence (Initialize (Macro i)) . 0 = i by A1, A2, GRFUNC_1:8; :: thesis: verum