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))],(insloc ((card I) + k))
let k be Element of NAT ; :: thesis: ProgramPart (Relocated (Directed I),k) = Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))
A1:
dom (ProgramPart I) = dom I
by AMI_1:105;
A2: dom (ProgramPart (Directed I)) =
dom (Directed I)
by AMI_1:105
.=
dom I
by FUNCT_4:105
;
then A3:
dom (ProgramPart (Relocated (Directed I),k)) = { (m + k) where m is Element of NAT : m in dom I }
by SCMFSA_5:3;
A4:
dom (ProgramPart (Relocated I,k)) = { (m + k) where m is Element of NAT : m in dom I }
by A1, SCMFSA_5:3;
then A5:
dom (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) = { (m + k) where m is Element of NAT : m in dom I }
by FUNCT_4:105;
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))],(insloc ((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))],(insloc ((card I) + k))) . xthen 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) . (insloc n) as
Instruction of
SCM+FSA by A8, AMI_1:126;
reconsider i0 =
I . (insloc n) as
Instruction of
SCM+FSA by A8, AMI_1:126;
A10:
(ProgramPart (Relocated (Directed I),k)) . x =
(Relocated (Directed I),k) . x
by A3, A6, Th49
.=
IncAddr i,
k
by A2, A8, A7, SCMFSA_5:7
;
now per cases
( i0 = halt SCM+FSA or i0 <> halt SCM+FSA )
;
suppose A11:
i0 = halt SCM+FSA
;
:: thesis: (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x = IncAddr i,kthen A12:
i = goto (insloc (card I))
by A8, FUNCT_4:112;
A13:
(ProgramPart (Relocated I,k)) . x =
(Relocated I,k) . x
by A4, A6, Th49
.=
IncAddr i0,
k
by A1, A8, A7, SCMFSA_5:7
.=
halt SCM+FSA
by A11, 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 (insloc ((card I) + k))))
by FUNCOP_1:19;
then A14:
x in dom (((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k)))
by A4, A6, FUNCT_1:21;
thus (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x =
(((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k))) . x
by A14, FUNCT_4:14
.=
((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) . ((ProgramPart (Relocated I,k)) . x)
by A4, A6, FUNCT_1:23
.=
goto (insloc ((card I) + k))
by A13, FUNCOP_1:87
.=
IncAddr i,
k
by A12, SCMFSA_4:14
;
:: thesis: verum end; suppose A15:
i0 <> halt SCM+FSA
;
:: thesis: (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x = IncAddr i,kthen
InsCode i0 <> 0
by SCMFSA_2:122;
then A16:
IncAddr i0,
k <> halt SCM+FSA
by SCMFSA_2:124, SCMFSA_4:22;
A17:
(ProgramPart (Relocated I,k)) . x =
(Relocated I,k) . x
by A4, A6, Th49
.=
IncAddr i0,
k
by A1, A8, A7, SCMFSA_5:7
;
then
not
(ProgramPart (Relocated I,k)) . x in {(halt SCM+FSA )}
by A16, TARSKI:def 1;
then
not
(ProgramPart (Relocated I,k)) . x in dom ((halt SCM+FSA ) .--> (goto (insloc ((card I) + k))))
by FUNCOP_1:19;
then A18:
not
x in dom (((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k)))
by FUNCT_1:21;
thus (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x =
[(ProgramPart (Relocated I,k))] . x
by A18, FUNCT_4:12
.=
IncAddr i,
k
by A15, A17, FUNCT_4:111
;
:: thesis: verum end; hence
(ProgramPart (Relocated (Directed I),k)) . x = (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x
by A10;
:: thesis: verum end;
hence
ProgramPart (Relocated (Directed I),k) = Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))
by A3, A5, FUNCT_1:9; :: thesis: verum