let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
A5: now :: thesis: for a being read-write Int-Location holds (Initialized s1) . a = (Initialized s2) . a
let a be read-write Int-Location; :: thesis: (Initialized s1) . a = (Initialized s2) . a
( a <> intloc 0 & a <> IC ) by SCMFSA_2:56;
then A6: not a in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
hence (Initialized s1) . a = s1 . a by FUNCT_4:11
.= s2 . a by A4
.= (Initialized s2) . a by A6, FUNCT_4:11 ;
:: thesis: verum
end;
assume A7: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
A8: now :: thesis: for f being FinSeq-Location holds (Initialized s1) . f = (Initialized s2) . f
let f be FinSeq-Location ; :: thesis: (Initialized s1) . f = (Initialized s2) . f
( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;
then A9: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
hence (Initialized s1) . f = s1 . f by FUNCT_4:11
.= s2 . f by A7
.= (Initialized s2) . f by A9, FUNCT_4:11 ;
:: thesis: verum
end;
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)) ; :: thesis: verum