let I be preProgram of SCM+FSA ; :: thesis: for k being Element of NAT holds ProgramPart (Relocated (Directed I),k) = Directed (ProgramPart (Relocated I,k)),((card I) + k)
let k be Element of NAT ; :: thesis: ProgramPart (Relocated (Directed I),k) = Directed (ProgramPart (Relocated I,k)),((card I) + k)
A1: dom (ProgramPart I) = dom I by AMI_1:105;
then A2: dom (ProgramPart (Relocated I,k)) = { (m + k) where m is Element of NAT : m in dom I } by SCMFSA_5:3;
A3: dom (ProgramPart (Directed I)) = dom (Directed I) by AMI_1:105
.= dom I by FUNCT_4:105 ;
then A4: dom (ProgramPart (Relocated (Directed I),k)) = { (m + k) where m is Element of NAT : m in dom I } by SCMFSA_5:3;

A5: now

let x be set ; :: thesis: ( x in { (m + k) where m is Element of NAT : m in dom I } implies (ProgramPart (Relocated (Directed I),k)) . x = (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x )
assume A6: x in { (m + k) where m is Element of NAT : m in dom I } ; :: thesis: (ProgramPart (Relocated (Directed I),k)) . x = (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x
then consider n being Element of NAT such that
A7: x = n + k and
A8: n in dom I ;
dom (Directed I) = dom I by FUNCT_4:105;
then reconsider i = (Directed I) . n as Instruction of SCM+FSA by A8, AMI_1:126;
reconsider i0 = I . n as Instruction of SCM+FSA by A8, AMI_1:126;

A9: now

per cases ( i0 = halt SCM+FSA or i0 <> halt SCM+FSA ) ;

suppose A10: i0 = halt SCM+FSA ; :: thesis: (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x = IncAddr i,k

then A11: i = goto (card I) by A8, FUNCT_4:112;
A12: (ProgramPart (Relocated I,k)) . x = (Relocated I,k) . x by A2, A6, Th64
.= IncAddr i0,k by A1, A7, A8, SCMFSA_5:7
.= halt SCM+FSA by A10, SCMFSA_4:8 ;
then (ProgramPart (Relocated I,k)) . x in {(halt SCM+FSA )} by TARSKI:def 1;
then (ProgramPart (Relocated I,k)) . x in dom ((halt SCM+FSA ) .--> (goto ((card I) + k))) by FUNCOP_1:19;
then x in dom (((halt SCM+FSA ) .--> (goto ((card I) + k))) * (ProgramPart (Relocated I,k))) by A2, A6, FUNCT_1:21;
hence (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x = (((halt SCM+FSA ) .--> (goto ((card I) + k))) * (ProgramPart (Relocated I,k))) . x by FUNCT_4:14
.= ((halt SCM+FSA ) .--> (goto ((card I) + k))) . ((ProgramPart (Relocated I,k)) . x) by A2, A6, FUNCT_1:23
.= goto ((card I) + k) by A12, FUNCOP_1:87
.= IncAddr i,k by A11, SCMFSA_4:14 ;
:: thesis: verum

end;

suppose A13: i0 <> halt SCM+FSA ; :: thesis: (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x = IncAddr i,k

A14: (ProgramPart (Relocated I,k)) . x = (Relocated I,k) . x by A2, A6, Th64
.= IncAddr i0,k by A1, A7, A8, SCMFSA_5:7 ;
InsCode i0 <> 0 by A13, SCMFSA_2:122;
then IncAddr i0,k <> halt SCM+FSA by SCMFSA_2:124, SCMFSA_4:22;
then not (ProgramPart (Relocated I,k)) . x in {(halt SCM+FSA )} by A14, TARSKI:def 1;
then not (ProgramPart (Relocated I,k)) . x in dom ((halt SCM+FSA ) .--> (goto ((card I) + k))) by FUNCOP_1:19;
then not x in dom (((halt SCM+FSA ) .--> (goto ((card I) + k))) * (ProgramPart (Relocated I,k))) by FUNCT_1:21;
hence (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x = (ProgramPart (Relocated I,k)) . x by FUNCT_4:12
.= IncAddr i,k by A13, A14, FUNCT_4:111 ;
:: thesis: verum

end;

end;

end;

(ProgramPart (Relocated (Directed I),k)) . x = (Relocated (Directed I),k) . x by A4, A6, Th64
.= IncAddr i,k by A3, A7, A8, SCMFSA_5:7 ;
hence (ProgramPart (Relocated (Directed I),k)) . x = (Directed (ProgramPart (Relocated I,k)),((card I) + k)) . x by A9; :: thesis: verum

end;

dom (Directed (ProgramPart (Relocated I,k)),((card I) + k)) = { (m + k) where m is Element of NAT : m in dom I } by A2, FUNCT_4:105;
hence ProgramPart (Relocated (Directed I),k) = Directed (ProgramPart (Relocated I,k)),((card I) + k) by A4, A5, FUNCT_1:9; :: thesis: verum