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 & ((Macro i) +* (Start-At (0,S))) . 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 & ((Macro i) +* (Start-At (0,S))) . 0 = i )
let i be Instruction of S; :: thesis: ( (Macro i) . 0 = i & (Macro i) . 1 = halt S & ((Macro i) +* (Start-At (0,S))) . 0 = i )
thus A1: (Macro i) . 0 = i by FUNCT_4:66; :: thesis: ( (Macro i) . 1 = halt S & ((Macro i) +* (Start-At (0,S))) . 0 = i )
thus (Macro i) . 1 = halt S by FUNCT_4:66; :: thesis: ((Macro i) +* (Start-At (0,S))) . 0 = i
A4: 0 in dom (Macro i) by Th147;
dom (Macro i) misses dom (Start-At (0,S)) by Th64;
then Macro i c= (Macro i) +* (Start-At (0,S)) by FUNCT_4:33;
hence ((Macro i) +* (Start-At (0,S))) . 0 = i by A1, A4, GRFUNC_1:8; :: thesis: verum