let I be preProgram of SCM+FSA; for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))
let k be Element of NAT ; Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))
A1:
dom (Reloc (I,k)) = { (m + k) where m is Nat : m in dom I }
by COMPOS_1:33;
A2:
dom (Directed I) = dom I
by FUNCT_4:99;
A3:
dom (Reloc ((Directed I),k)) = { (m + k) where m is Nat : m in dom I }
by A2, COMPOS_1:33;
A4:
now for x being object st x in { (m + k) where m is Nat : m in dom I } holds
(Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . xlet x be
object ;
( x in { (m + k) where m is Nat : m in dom I } implies (Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x )assume A5:
x in { (m + k) where m is Nat : m in dom I }
;
(Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . xthen consider n being
Nat such that A6:
x = n + k
and A7:
n in dom I
;
dom (Directed I) = dom I
by FUNCT_4:99;
then reconsider i =
(Directed I) . n as
Instruction of
SCM+FSA by A7, FUNCT_1:106;
reconsider i0 =
I . n as
Instruction of
SCM+FSA by A7, FUNCT_1:106;
A8:
now ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)per cases
( i0 = halt SCM+FSA or i0 <> halt SCM+FSA )
;
suppose A9:
i0 = halt SCM+FSA
;
((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)then A10:
i = goto (card I)
by A7, FUNCT_4:106;
A11:
(Reloc (I,k)) . x =
IncAddr (
i0,
k)
by A6, A7, COMPOS_1:35
.=
halt SCM+FSA
by A9, COMPOS_0:4
;
then
(Reloc (I,k)) . x in {(halt SCM+FSA)}
by TARSKI:def 1;
then
(Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k)))
;
then
x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k)))
by A1, A5, FUNCT_1:11;
hence ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x =
(((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) . x
by FUNCT_4:13
.=
((halt SCM+FSA) .--> (goto ((card I) + k))) . ((Reloc (I,k)) . x)
by A1, A5, FUNCT_1:13
.=
goto ((card I) + k)
by A11, FUNCOP_1:72
.=
IncAddr (
i,
k)
by A10, SCMFSA_4:1
;
verum end; suppose A12:
i0 <> halt SCM+FSA
;
((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x = IncAddr (i,k)A13:
(Reloc (I,k)) . x = IncAddr (
i0,
k)
by A6, A7, COMPOS_1:35;
A14:
InsCode (halt SCM+FSA) = 0
by COMPOS_1:70;
InsCode i0 <> 0
by A12, SCMFSA_2:95;
then
IncAddr (
i0,
k)
<> halt SCM+FSA
by A14, COMPOS_0:def 9;
then
not
(Reloc (I,k)) . x in {(halt SCM+FSA)}
by A13, TARSKI:def 1;
then
not
(Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k)))
;
then
not
x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k)))
by FUNCT_1:11;
hence ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x =
(Reloc (I,k)) . x
by FUNCT_4:11
.=
IncAddr (
i,
k)
by A12, A13, FUNCT_4:105
;
verum end; end; end; thus
(Reloc ((Directed I),k)) . x = ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) . x
by A8, A2, A6, A7, COMPOS_1:35;
verum end;
dom ((Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))) = { (m + k) where m is Nat : m in dom I }
by A1, FUNCT_4:99;
hence
Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))
by A3, A4, FUNCT_1:2; verum