let m be Nat; :: thesis: for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
let I be Program of ; :: thesis: Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
rng ((halt SCM+FSA) .--> (goto (card I))) = {(goto (card I))} by FUNCOP_1:8;
then A1: rng ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I)))) c= (rng (id the InstructionsF of SCM+FSA)) \/ {(goto (card I))} by FUNCT_4:17;
A2: (rng (id the InstructionsF of SCM+FSA)) \/ {(goto (card I))} = the InstructionsF of SCM+FSA by ZFMISC_1:40;
dom ((halt SCM+FSA) .--> (goto (card I))) = {(halt SCM+FSA)} ;
then dom ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I)))) = (dom (id the InstructionsF of SCM+FSA)) \/ {(halt SCM+FSA)} by FUNCT_4:def 1
.= the InstructionsF of SCM+FSA by ZFMISC_1:40 ;
then reconsider f = (id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I))) as Function of the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA by A1, A2, FUNCT_2:def 1, RELSET_1:4;
A3: IncAddr ((goto (card I)),m) = goto (m + (card I)) by SCMFSA_4:1;
dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ;
then A4: f = (id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))) by FUNCT_7:def 3;
A5: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
A6: Reloc ((Directed I),m) = IncAddr ((Shift ((Directed I),m)),m) by COMPOS_1:34;
A7: Reloc (I,m) = IncAddr ((Shift (I,m)),m) by COMPOS_1:34;
Directed I = f * I by A4, A5, FUNCT_7:116;
hence Reloc ((Directed I),m) = IncAddr ((f * (Shift (I,m))),m) by A6, VALUED_1:22
.= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m)) by A3, A7, COMPOS_1:47 ;
:: thesis: verum