let m be Element of NAT ; :: thesis: for I being Program of SCM+FSA holds ProgramPart (Relocated (Directed I),m) = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (m + (card I))))) * (ProgramPart (Relocated I,m))
let I be Program of SCM+FSA ; :: thesis: ProgramPart (Relocated (Directed I),m) = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (m + (card I))))) * (ProgramPart (Relocated I,m))
A1: dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
rng ((halt SCM+FSA ) .--> (goto (card I))) = {(goto (card I))} by FUNCOP_1:14;
then A2: rng ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (card I)))) c= (rng (id the Instructions of SCM+FSA )) \/ {(goto (card I))} by FUNCT_4:18;
rng (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then A3: (rng (id the Instructions of SCM+FSA )) \/ {(goto (card I))} = the Instructions of SCM+FSA by ZFMISC_1:46;
dom ((halt SCM+FSA ) .--> (goto (card I))) = {(halt SCM+FSA )} by FUNCOP_1:19;
then dom ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (card I)))) = (dom (id the Instructions of SCM+FSA )) \/ {(halt SCM+FSA )} by FUNCT_4:def 1
.= the Instructions of SCM+FSA by A1, ZFMISC_1:46 ;
then reconsider f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (card I))) as Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA by A2, A3, FUNCT_2:def 1, RELSET_1:11;
A4: IncAddr (goto (card I)),m = goto (m + (card I)) by SCMFSA_4:14;
dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then A5: f = (id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto (card I)) by FUNCT_7:def 3;
A6: ProgramPart I = I by RELAT_1:209;
A7: rng I c= the Instructions of SCM+FSA by RELAT_1:def 19;
ProgramPart (Directed I) = Directed I by RELAT_1:209
.= f * I by A5, A7, FUNCT_7:118 ;
hence ProgramPart (Relocated (Directed I),m) = Reloc (f * I),m by AMISTD_2:69
.= IncAddr (f * (Shift I,m)),m by VALUED_1:23
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (m + (card I))))) * (Reloc I,m) by A4, SCMFSA_4:26
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (m + (card I))))) * (ProgramPart (Relocated I,m)) by A6, AMISTD_2:69 ;
:: thesis: verum