let IT, s be PartState of SCM+FSA; ( IT = s +* (Initialize ((intloc 0) .--> 1)) implies IT = IT +* (Initialize ((intloc 0) .--> 1)) )
assume A1:
IT = s +* (Initialize ((intloc 0) .--> 1))
; IT = IT +* (Initialize ((intloc 0) .--> 1))
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:13;
then A2:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
A3:
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (s +* ((intloc 0) .--> 1))
by FUNCT_4:14;
dom ((intloc 0) .--> 1) = {(intloc 0)}
by FUNCOP_1:13;
then A4:
intloc 0 in dom ((intloc 0) .--> 1)
by TARSKI:def 1;
A5:
not intloc 0 in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
A6: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) =
(Initialize (s +* ((intloc 0) .--> 1))) . (intloc 0)
by FUNCT_4:14
.=
(s +* ((intloc 0) .--> 1)) . (intloc 0)
by A5, FUNCT_4:11
.=
((intloc 0) .--> 1) . (intloc 0)
by A4, FUNCT_4:13
.=
1
by FUNCOP_1:72
;
(Start-At (0,SCM+FSA)) . (IC ) = 0
by FUNCOP_1:72;
then A7:
IC IT = 0
by A1, A2, A3, FUNCT_4:13;
A8:
IC in dom IT
by A1, MEMSTR_0:49;
A9:
dom IT = (dom s) \/ (dom (Initialize ((intloc 0) .--> 1)))
by A1, FUNCT_4:def 1;
A10:
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA)))
by FUNCT_4:def 1;
dom ((intloc 0) .--> 1) = {(intloc 0)}
by FUNCOP_1:13;
then
intloc 0 in dom ((intloc 0) .--> 1)
by TARSKI:def 1;
then
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
by A10, XBOOLE_0:def 3;
then A11:
intloc 0 in dom IT
by A9, XBOOLE_0:def 3;
thus IT +* (Initialize ((intloc 0) .--> 1)) =
Initialize (IT +* ((intloc 0) .--> 1))
by FUNCT_4:14
.=
IT +* ((IC ) .--> 0)
by A6, A11, A1, FUNCT_7:109
.=
IT
by A7, A8, FUNCT_7:109
; verum