let S be COM-Struct ; for n being Nat
for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
let n be Nat; for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
let i be Instruction of S; Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
A1: dom (Macro (IncAddr (i,n))) =
{0,1}
by Th45
.=
dom (Macro i)
by Th45
;
for m being Nat st m in dom (Macro i) holds
(Macro (IncAddr (i,n))) . m = IncAddr (((Macro i) /. m),n)
hence
Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
by A1, Def9; verum