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 (insloc (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 (insloc (m + (card I)))))) * (ProgramPart (Relocated I,m))
A1: dom ((halt SCM+FSA ) .--> (goto (insloc (card I)))) = {(halt SCM+FSA )} by FUNCOP_1:19;
A2: rng ((halt SCM+FSA ) .--> (goto (insloc (card I)))) = {(goto (insloc (card I)))} by FUNCOP_1:14;
A3: dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
A4: dom ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (card I))))) = (dom (id the Instructions of SCM+FSA )) \/ {(halt SCM+FSA )} by A1, FUNCT_4:def 1
.= the Instructions of SCM+FSA by A3, ZFMISC_1:46 ;
A5: rng (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
A6: rng ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (card I))))) c= (rng (id the Instructions of SCM+FSA )) \/ {(goto (insloc (card I)))} by A2, FUNCT_4:18;
(rng (id the Instructions of SCM+FSA )) \/ {(goto (insloc (card I)))} = the Instructions of SCM+FSA by A5, ZFMISC_1:46;
then reconsider f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (card I)))) as Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA by A4, A6, FUNCT_2:def 1, RELSET_1:11;
dom (id the Instructions of SCM+FSA ) = the Instructions of SCM+FSA by RELAT_1:71;
then U: f = (id the Instructions of SCM+FSA ) +* (halt SCM+FSA ),(goto (insloc (card I))) by FUNCT_7:def 3;
A7: IncAddr (goto (insloc (card I))),m = goto (insloc (m + (card I))) by SCMFSA_4:14;
Y: rng I c= the Instructions of SCM+FSA by AMI_1:118;
X: ProgramPart I = I by AMI_1:105;
ProgramPart (Directed I) = Directed I by AMI_1:105
.= f * I by Y, U, FUNCT_7:118 ;
hence ProgramPart (Relocated (Directed I),m) = IncAddr (Shift (f * I),m),m by SCMFSA_5:2
.= IncAddr (f * (Shift I,m)),m by VALUED_1:23
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (m + (card I)))))) * (IncAddr (Shift I,m),m) by A7, SCMFSA_4:26
.= ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc (m + (card I)))))) * (ProgramPart (Relocated I,m)) by X, SCMFSA_5:2 ;
:: thesis: verum