let S be COM-Struct ; :: thesis: for n being Nat
for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
let n be Nat; :: thesis: for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)
let i be Instruction of S; :: thesis: 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)
proof
let m be Nat; :: thesis: ( m in dom (Macro i) implies (Macro (IncAddr (i,n))) . m = IncAddr (((Macro i) /. m),n) )
assume m in dom (Macro i) ; :: thesis: (Macro (IncAddr (i,n))) . m = IncAddr (((Macro i) /. m),n)
per cases then ( m = 0 or m = 1 ) by Th44;
suppose A2: m = 0 ; :: thesis: (Macro (IncAddr (i,n))) . m = IncAddr (((Macro i) /. m),n)
then m in dom (Macro i) by Th41;
then A3: (Macro i) /. m = (Macro i) . m by PARTFUN1:def 6
.= i by A2, Th42 ;
thus (Macro (IncAddr (i,n))) . m = IncAddr (i,n) by A2, Th42
.= IncAddr (((Macro i) /. m),n) by A3 ; :: thesis: verum
end;
suppose A4: m = 1 ; :: thesis: (Macro (IncAddr (i,n))) . m = IncAddr (((Macro i) /. m),n)
then m in dom (Macro i) by Th41;
then A5: (Macro i) /. m = (Macro i) . m by PARTFUN1:def 6
.= halt S by A4, Th43 ;
thus (Macro (IncAddr (i,n))) . m = halt S by Th43, A4
.= IncAddr ((halt S),n) by COMPOS_0:4
.= IncAddr (((Macro i) /. m),n) by A5 ; :: thesis: verum
end;
end;
end;
hence Macro (IncAddr (i,n)) = IncAddr ((Macro i),n) by A1, Def9; :: thesis: verum