let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & 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 Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & 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 SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & 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 = s1 +* (Initialize ((intloc 0) .--> 1));
set P11 = P1 +* I;
set s21 = s2 +* (Initialize ((intloc 0) .--> 1));
set P21 = P2 +* I;
A1: Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s1 +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A2: Start-At (0,SCM+FSA) c= s1 +* (Initialize ((intloc 0) .--> 1)) by A1, XBOOLE_1:1;
Initialize ((intloc 0) .--> 1) c= s2 +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A3: Start-At (0,SCM+FSA) c= s2 +* (Initialize ((intloc 0) .--> 1)) by A1, XBOOLE_1:1;
assume s1 . (intloc 0) = 1 ; :: thesis: ( not I is_closed_on s1,P1 or 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 A4: s1 +* (Initialize ((intloc 0) .--> 1)) = Initialize s1 by Th18;
then A5: DataPart (s1 +* (Initialize ((intloc 0) .--> 1))) = DataPart s1 by SCMFSA8A:10;
assume that
A6: I is_closed_on s1,P1 and
A7: 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)) )
A8: I is_closed_on s1 +* (Initialize ((intloc 0) .--> 1)),P1 +* I by A6, A7, A5, SCMFSA8B:8;
assume A9: 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)) )
Initialize ((intloc 0) .--> 1) c= Initialized I by FUNCT_4:26;
then X1: dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized I) by RELAT_1:25;

A10: now

let a be read-write Int-Location ; :: thesis: (s1 +* (Initialize ((intloc 0) .--> 1))) . a = (s2 +* (Initialize ((intloc 0) .--> 1))) . a
A11: not a in dom (Initialize ((intloc 0) .--> 1)) by X1, SCMFSA6A:48;
hence (s1 +* (Initialize ((intloc 0) .--> 1))) . a = s1 . a by FUNCT_4:12
.= s2 . a by A9
.= (s2 +* (Initialize ((intloc 0) .--> 1))) . a by A11, FUNCT_4:12 ;
:: thesis: verum

end;

assume A12: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

A13: now

let f be FinSeq-Location ; :: thesis: (s1 +* (Initialize ((intloc 0) .--> 1))) . f = (s2 +* (Initialize ((intloc 0) .--> 1))) . f
A14: not f in dom (Initialize ((intloc 0) .--> 1)) by X1, SCMFSA6A:49;
hence (s1 +* (Initialize ((intloc 0) .--> 1))) . f = s1 . f by FUNCT_4:12
.= s2 . f by A12
.= (s2 +* (Initialize ((intloc 0) .--> 1))) . f by A14, FUNCT_4:12 ;
:: thesis: verum

end;

A15: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:86;
then (s1 +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:14
.= (s2 +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) by A15, FUNCT_4:14 ;
then A16: DataPart (s1 +* (Initialize ((intloc 0) .--> 1))) = DataPart (s2 +* (Initialize ((intloc 0) .--> 1))) by A10, A13, Th33;
A18: I c= P2 +* I by FUNCT_4:26;
A19: I c= P1 +* I by FUNCT_4:26;
A20: P1 +* I halts_on s1 +* (Initialize ((intloc 0) .--> 1)) by A7, A4, SCMFSA7B:def 8;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1)))))))) = halt SCM+FSA by EXTPRO_1:def 14;
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1)))))))) = halt SCM+FSA by A8, A16, A2, A3, Th43, A19, A18;
then A21: P2 +* I halts_on s2 +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:30;
I is_halting_on s1 +* (Initialize ((intloc 0) .--> 1)),P1 +* I by A6, A7, A5, SCMFSA8B:8;
then A22: LifeSpan ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((P2 +* I),(s2 +* (Initialize ((intloc 0) .--> 1)))) by A8, A16, A2, A3, Th44, A19, A18;
thus DataPart (IExec (I,P1,s1)) = DataPart (Result ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1))))) by SCMFSA8B:35
.= DataPart (Comput ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1))))))) by A20, EXTPRO_1:23
.= DataPart (Comput ((P2 +* I),(s2 +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P1 +* I),(s1 +* (Initialize ((intloc 0) .--> 1))))))) by A8, A16, A2, A3, Th43, A19, A18
.= DataPart (Result ((P2 +* I),(s2 +* (Initialize ((intloc 0) .--> 1))))) by A22, A21, EXTPRO_1:23
.= DataPart (IExec (I,P2,s2)) by SCMFSA8B:35 ; :: thesis: verum