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;
then A2:
dom (ProgramPart (Relocated I,k)) = { (m + k) where m is Element of NAT : m in dom I }
by SCMFSA_5:3;
A3: dom (ProgramPart (Directed I)) =
dom (Directed I)
by AMI_1:105
.=
dom I
by FUNCT_4:105
;
then A4:
dom (ProgramPart (Relocated (Directed I),k)) = { (m + k) where m is Element of NAT : m in dom I }
by SCMFSA_5:3;
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))],(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;
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))],(insloc ((card I) + k))) . x = IncAddr i,kthen A11:
i = goto (insloc (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, SCMFSA_5:7
.=
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 (insloc ((card I) + k))))
by FUNCOP_1:19;
then
x in dom (((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k)))
by A2, A6, FUNCT_1:21;
hence (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x =
(((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k))) . x
by FUNCT_4:14
.=
((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) . ((ProgramPart (Relocated I,k)) . x)
by A2, A6, FUNCT_1:23
.=
goto (insloc ((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))],(insloc ((card I) + k))) . x = IncAddr i,kA14:
(ProgramPart (Relocated I,k)) . x =
(Relocated I,k) . x
by A2, A6, Th64
.=
IncAddr i0,
k
by A1, A7, A8, SCMFSA_5:7
;
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 (insloc ((card I) + k))))
by FUNCOP_1:19;
then
not
x in dom (((halt SCM+FSA ) .--> (goto (insloc ((card I) + k)))) * (ProgramPart (Relocated I,k)))
by FUNCT_1:21;
hence (Directed [(ProgramPart (Relocated I,k))],(insloc ((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; (ProgramPart (Relocated (Directed I),k)) . x =
(Relocated (Directed I),k) . x
by A4, A6, Th64
.=
IncAddr i,
k
by A3, A7, A8, SCMFSA_5:7
;
hence
(ProgramPart (Relocated (Directed I),k)) . x = (Directed [(ProgramPart (Relocated I,k))],(insloc ((card I) + k))) . x
by A9;
:: thesis: verum end;
dom (Directed [(ProgramPart (Relocated I,k))],(insloc ((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))],(insloc ((card I) + k))
by A4, A5, FUNCT_1:9; :: thesis: verum