let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_closed_on Initialized s1 & I is_halting_on Initialized s1 holds
( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) )
let I be Program of SCM+FSA; :: thesis: for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_closed_on Initialized s1 & I is_halting_on Initialized s1 holds
( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) )
let a be Int-Location ; :: thesis: ( ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_closed_on Initialized s1 & I is_halting_on Initialized s1 implies ( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) ) )
assume that
A1: for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d and
A2: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: ( I refers a or not I is_closed_on Initialized s1 or not I is_halting_on Initialized s1 or ( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) ) )

A3: now

let d be Int-Location ; :: thesis: ( a <> d implies (Initialized s1) . b₁ = (Initialized s2) . b₁ )
assume A4: a <> d ; :: thesis: (Initialized s1) . b₁ = (Initialized s2) . b₁

per cases ( d = intloc 0 or d <> intloc 0 ) ;

suppose A5: d = intloc 0 ; :: thesis: (Initialized s1) . b₁ = (Initialized s2) . b₁

hence (Initialized s1) . d = 1 by SCMFSA6C:3
.= (Initialized s2) . d by A5, SCMFSA6C:3 ;
:: thesis: verum

end;

suppose d <> intloc 0 ; :: thesis: (Initialized s1) . b₁ = (Initialized s2) . b₁

then A6: not d is read-only by SF_MASTR:def 5;
hence (Initialized s1) . d = s1 . d by SCMFSA6C:3
.= s2 . d by A1, A4, A6
.= (Initialized s2) . d by A6, SCMFSA6C:3 ;
:: thesis: verum

end;

end;

end;

set S1 = s1 +* (Initialized I);
set S2 = s2 +* (Initialized I);
assume A7: not I refers a ; :: thesis: ( not I is_closed_on Initialized s1 or not I is_halting_on Initialized s1 or ( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) ) )
A8: s2 +* (Initialized I) = (Initialized s2) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
assume that
A9: I is_closed_on Initialized s1 and
A10: I is_halting_on Initialized s1 ; :: thesis: ( ( for d being Int-Location st a <> d holds
(IExec (I,s1)) . d = (IExec (I,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) )

A11: now

let f be FinSeq-Location ; :: thesis: (Initialized s1) . f = (Initialized s2) . f
thus (Initialized s1) . f = s1 . f by SCMFSA6C:3
.= s2 . f by A2
.= (Initialized s2) . f by SCMFSA6C:3 ; :: thesis: verum

end;

then I is_halting_on Initialized s2 by A7, A9, A10, A3, Th40;
then A12: ProgramPart (s2 +* (Initialized I)) halts_on s2 +* (Initialized I) by A8, SCMFSA7B:def 8;
A13: s1 +* (Initialized I) = (Initialized s1) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A14: ProgramPart (s1 +* (Initialized I)) halts_on s1 +* (Initialized I) by A10, SCMFSA7B:def 8;

now

let l be Element of NAT ; :: thesis: ( l < LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) implies CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l))) <> halt SCM+FSA )
TX1: ProgramPart (s1 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),l)) by AMI_1:123;
TX2: ProgramPart (s2 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l)) by AMI_1:123;
assume l < LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) ; :: thesis: CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l))) <> halt SCM+FSA
then CurInstr ((ProgramPart (s1 +* (Initialized I))),(Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),l))) <> halt SCM+FSA by A14, EXTPRO_1:def 14;
hence CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l))) <> halt SCM+FSA by A7, A9, A3, A11, A13, A8, Th38, TX1, TX2; :: thesis: verum

end;

then A15: for l being Element of NAT st CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l))) = halt SCM+FSA holds
LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) <= l ;
TX1: ProgramPart (s1 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
TX2: ProgramPart (s2 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) = CurInstr ((ProgramPart (s1 +* (Initialized I))),(Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) by A7, A9, A3, A11, A13, A8, Th38, TX1, TX2
.= halt SCM+FSA by A14, EXTPRO_1:def 14 ;
then A16: LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) = LifeSpan ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I))) by A12, A15, EXTPRO_1:def 14;
then A17: Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I))) = Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))) by A12, EXTPRO_1:23;
A18: Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) = Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))) by A14, EXTPRO_1:23;

hereby :: thesis: ( ( for f being FinSeq-Location holds (IExec (I,s1)) . f = (IExec (I,s2)) . f ) & IC (IExec (I,s1)) = IC (IExec (I,s2)) )

let d be Int-Location ; :: thesis: ( a <> d implies (IExec (I,s1)) . d = (IExec (I,s2)) . d )
assume A19: a <> d ; :: thesis: (IExec (I,s1)) . d = (IExec (I,s2)) . d
thus (IExec (I,s1)) . d = (Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))) . d by Th36, SCMFSA10:92
.= (Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))) . d by A7, A9, A3, A11, A13, A8, A17, A18, A19, Th38
.= (IExec (I,s2)) . d by Th36, SCMFSA10:92 ; :: thesis: verum

end;

hereby :: thesis: IC (IExec (I,s1)) = IC (IExec (I,s2))

let f be FinSeq-Location ; :: thesis: (IExec (I,s1)) . f = (IExec (I,s2)) . f
thus (IExec (I,s1)) . f = (Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))) . f by Th36, SCMFSA10:93
.= (Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))) . f by A7, A9, A3, A11, A13, A8, A17, A18, Th38
.= (IExec (I,s2)) . f by Th36, SCMFSA10:93 ; :: thesis: verum

end;

thus IC (IExec (I,s1)) = IC (Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))) by SCMFSA8A:7
.= IC (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by A14, EXTPRO_1:23
.= IC (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))))) by A7, A9, A3, A11, A13, A8, A16, Th38
.= IC (Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))) by A12, EXTPRO_1:23
.= IC (IExec (I,s2)) by SCMFSA8A:7 ; :: thesis: verum