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 ) & I does_not_refer a & I is_closed_on Initialize s1 & I is_halting_on Initialize 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 ) & I does_not_refer a & I is_closed_on Initialize s1 & I is_halting_on Initialize 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 ) & I does_not_refer a & I is_closed_on Initialize s1 & I is_halting_on Initialize 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: ( not I does_not_refer a or not I is_closed_on Initialize s1 or not I is_halting_on Initialize 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 (Initialize s1) . b₁ = (Initialize s2) . b₁ )
assume A4: a <> d ; :: thesis: (Initialize s1) . b₁ = (Initialize s2) . b₁

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

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

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

end;

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

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

end;

end;

end;

set S1 = s1 +* (Initialized I);
set S2 = s2 +* (Initialized I);
assume A7: I does_not_refer a ; :: thesis: ( not I is_closed_on Initialize s1 or not I is_halting_on Initialize 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) = (Initialize s2) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
assume that
A9: I is_closed_on Initialize s1 and
A10: I is_halting_on Initialize 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: (Initialize s1) . f = (Initialize s2) . f
thus (Initialize s1) . f = s1 . f by SCMFSA6C:3
.= s2 . f by A2
.= (Initialize s2) . f by SCMFSA6C:3 ; :: thesis: verum

end;

then I is_halting_on Initialize 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) = (Initialize 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 (s1 +* (Initialized I)) implies CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l)),(Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l) <> halt SCM+FSA )
assume l < LifeSpan (s1 +* (Initialized I)) ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l)),(Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l) <> halt SCM+FSA
then CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),l)),(Comput (ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),l) <> halt SCM+FSA by A14, AMI_1:def 46;
hence CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l)),(Comput (ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),l) <> halt SCM+FSA by A7, A9, A3, A11, A13, A8, Th38; :: thesis: verum

end;

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

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 (s1 +* (Initialized I))) . d by Th36, SCMFSA6A:30
.= (Result (s2 +* (Initialized I))) . d by A7, A9, A3, A11, A13, A8, A17, A18, A19, Th38
.= (IExec I,s2) . d by Th36, SCMFSA6A:30 ; :: 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 (s1 +* (Initialized I))) . f by Th36, SCMFSA6A:31
.= (Result (s2 +* (Initialized I))) . f by A7, A9, A3, A11, A13, A8, A17, A18, Th38
.= (IExec I,s2) . f by Th36, SCMFSA6A:31 ; :: thesis: verum

end;

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