let S be COM-Struct ; :: thesis: for n being Nat
for i being Instruction of S holds IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)
let n be Nat; :: thesis: for i being Instruction of S holds IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)
let i be Instruction of S; :: thesis: IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)
A1: dom (Macro i) = {0,1} by Th45;
A2: dom ((IncAddr ((Load i),n)) ^ (Stop S)) = len ((IncAddr ((Load i),n)) ^ (Stop S))
.= (len (IncAddr ((Load i),n))) + 1 by AFINSQ_1:75
.= (len (Load i)) + 1 by Def9
.= 1 + 1 by AFINSQ_1:34
.= {0,1} by CARD_1:50
.= dom (Macro i) by Th45 ;
for m being Nat st m in dom (Macro i) holds
((IncAddr ((Load i),n)) ^ (Stop S)) . m = IncAddr (((Macro i) /. m),n)
proof
let m be Nat; :: thesis: ( m in dom (Macro i) implies ((IncAddr ((Load i),n)) ^ (Stop S)) . m = IncAddr (((Macro i) /. m),n) )
assume m in dom (Macro i) ; :: thesis: ((IncAddr ((Load i),n)) ^ (Stop S)) . m = IncAddr (((Macro i) /. m),n)
per cases then ( m = 0 or m = 1 ) by A1, TARSKI:def 2;
suppose A3: m = 0 ; :: thesis: ((IncAddr ((Load i),n)) ^ (Stop S)) . m = IncAddr (((Macro i) /. m),n)
A4: 0 in dom (Load i) by AFINSQ_1:65;
then A5: (Load i) /. m = (Load i) . m by A3, PARTFUN1:def 6;
dom (Load i) c= dom ((Load i) ^ (Stop S)) by AFINSQ_1:21;
then m in dom ((Load i) ^ (Stop S)) by A4, A3;
then A6: ((Load i) ^ (Stop S)) . m = ((Load i) ^ (Stop S)) /. m by PARTFUN1:def 6;
m in dom (IncAddr ((Load i),n)) by Def9, A4, A3;
hence ((IncAddr ((Load i),n)) ^ (Stop S)) . m = (IncAddr ((Load i),n)) . m by AFINSQ_1:def 3
.= IncAddr (((Load i) /. m),n) by A4, Def9, A3
.= IncAddr (((stop (Load i)) /. m),n) by A6, A4, AFINSQ_1:def 3, A5, A3
.= IncAddr (((Macro i) /. m),n) ;
:: thesis: verum
end;
suppose A7: m = 1 ; :: thesis: ((IncAddr ((Load i),n)) ^ (Stop S)) . m = IncAddr (((Macro i) /. m),n)
A8: len (Load i) = 1 by AFINSQ_1:34;
then A9: len (IncAddr ((Load i),n)) = 1 by Def9;
A10: 0 in dom (Stop S) by AFINSQ_1:65;
len ((Load i) ^ (Stop S)) = (len (Load i)) + (len (Stop S)) by AFINSQ_1:def 3
.= (len (Load i)) + 1 by AFINSQ_1:34
.= 1 + 1 by AFINSQ_1:34
.= {0,1} by CARD_1:50 ;
then 1 in dom ((Load i) ^ (Stop S)) by TARSKI:def 2;
then A11: ((Load i) ^ (Stop S)) /. m = ((Load i) ^ (Stop S)) . (1 + 0) by PARTFUN1:def 6, A7;
A12: (Stop S) /. 0 = (Stop S) . 0 by A10, PARTFUN1:def 6;
thus ((IncAddr ((Load i),n)) ^ (Stop S)) . m = ((IncAddr ((Load i),n)) ^ (Stop S)) . (1 + 0) by A7
.= (IncAddr ((Stop S),n)) . 0 by AFINSQ_1:def 3, A9, A10
.= IncAddr (((Stop S) /. 0),n) by A10, Def9
.= IncAddr (((stop (Load i)) /. m),n) by A11, A12, AFINSQ_1:def 3, A8, A10
.= IncAddr (((Macro i) /. m),n) ; :: thesis: verum
end;
end;
end;
hence IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S) by A2, Def9; :: thesis: verum