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 RELAT_1:209;
A2: dom (ProgramPart (Relocated (I,k))) = dom (Reloc ((ProgramPart I),k)) by COMPOS_1:116
.= { (m + k) where m is Element of NAT : m in dom I } by A1, COMPOS_1:117 ;
A3: dom (ProgramPart (Directed I)) = dom (Directed I) by RELAT_1:209
.= dom I by FUNCT_4:105 ;
A4: dom (ProgramPart (Relocated ((Directed I),k))) = dom (Reloc ((ProgramPart (Directed I)),k)) by COMPOS_1:116
.= { (m + k) where m is Element of NAT : m in dom I } by A3, COMPOS_1:117 ;

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, FUNCT_1:176;
reconsider i0 = I . n as Instruction of SCM+FSA by A8, FUNCT_1:176;

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, COMPOS_1:122
.= 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, COMPOS_1:122 ;
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, COMPOS_1:122 ;
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