let IT, s be PartState of SCM+FSA; ( IT = s +* (Initialize ((intloc 0) .--> 1)) implies IT = IT +* (Initialize ((intloc 0) .--> 1)) )
assume Z:
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 A5:
intloc 0 in dom ((intloc 0) .--> 1)
by TARSKI:def 1;
A6:
not intloc 0 in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
B1: (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 A6, FUNCT_4:11
.=
((intloc 0) .--> 1) . (intloc 0)
by A5, FUNCT_4:13
.=
1
by FUNCOP_1:72
;
(Start-At (0,SCM+FSA)) . (IC ) = 0
by FUNCOP_1:72;
then B2:
IC IT = 0
by Z, A2, A3, FUNCT_4:13;
A3:
IC in dom IT
by Z, MEMSTR_0:49;
X1:
dom IT = (dom s) \/ (dom (Initialize ((intloc 0) .--> 1)))
by Z, FUNCT_4:def 1;
X2:
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 X2, XBOOLE_0:def 3;
then A4:
intloc 0 in dom IT
by X1, XBOOLE_0:def 3;
thus IT +* (Initialize ((intloc 0) .--> 1)) =
Initialize (IT +* ((intloc 0) .--> 1))
by FUNCT_4:14
.=
IT +* ((IC ) .--> 0)
by B1, A4, Z, FUNCT_7:109
.=
IT
by B2, A3, FUNCT_7:109
; verum