let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
let s1, s2 be State of SCM+FSA; for I being really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
set D = Data-Locations ;
let I be really-closed Program of SCM+FSA; ( s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
set s11 = Initialized s1;
set P11 = P1 +* I;
set s21 = Initialized s2;
set P21 = P2 +* I;
assume
s1 . (intloc 0) = 1
; ( not I is_halting_on s1,P1 or ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
then A1:
Initialized s1 = Initialize s1
by SCMFSA_M:18;
then A2:
DataPart (Initialized s1) = DataPart s1
by MEMSTR_0:79;
assume A3:
I is_halting_on s1,P1
; ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
assume A4:
for a being read-write Int-Location holds s1 . a = s2 . a
; ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
assume A7:
for f being FinSeq-Location holds s1 . f = s2 . f
; DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
A10:
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA_M:10;
then (Initialized s1) . (intloc 0) =
(Initialize ((intloc 0) .--> 1)) . (intloc 0)
by FUNCT_4:13
.=
(Initialized s2) . (intloc 0)
by A10, FUNCT_4:13
;
then A11:
DataPart (Initialized s1) = DataPart (Initialized s2)
by A5, A8, SCMFSA_M:20;
A12:
I c= P2 +* I
by FUNCT_4:25;
A13:
I c= P1 +* I
by FUNCT_4:25;
A14:
P1 +* I halts_on Initialized s1
by A3, A1;
then
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA
by EXTPRO_1:def 15;
then
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA
by A11, Th9, A13, A12;
then A15:
P2 +* I halts_on Initialized s2
by EXTPRO_1:29;
I is_halting_on Initialized s1,P1 +* I
by A3, A2, SCMFSA8B:5;
then A16:
LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2))
by A11, Th10, A13, A12;
thus DataPart (IExec (I,P1,s1)) =
DataPart (Result ((P1 +* I),(Initialized s1)))
.=
DataPart (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))
by A14, EXTPRO_1:23
.=
DataPart (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))
by A11, Th9, A13, A12
.=
DataPart (Result ((P2 +* I),(Initialized s2)))
by A16, A15, EXTPRO_1:23
.=
DataPart (IExec (I,P2,s2))
; verum