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 A1: ( ( 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 ) ) ; :: 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) ) )
assume A2: 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) ) )
assume A3: ( I is_closed_on Initialize s1 & 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) )

A4: now

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

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

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

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

end;

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

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

end;

end;

end;

A8: 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 A1
.= (Initialize s2) . f by SCMFSA6C:3 ; :: thesis: verum

end;

then A9: ( I is_closed_on Initialize s2 & I is_halting_on Initialize s2 ) by A2, A3, A4, Th40;
set S1 = s1 +* (Initialized I);
set S2 = s2 +* (Initialized I);
A10: s1 +* (Initialized I) = (Initialize s1) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A11: s1 +* (Initialized I) is halting by A3, SCMFSA7B:def 8;
A12: s2 +* (Initialized I) = (Initialize s2) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A13: s2 +* (Initialized I) is halting by A9, SCMFSA7B:def 8;
A14: CurInstr (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = CurInstr (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A2, A3, A4, A8, A10, A12, Th38
.= halt SCM+FSA by A11, AMI_1:def 46 ;

now

let l be Element of NAT ; :: thesis: ( l < LifeSpan (s1 +* (Initialized I)) implies CurInstr (Computation (s2 +* (Initialized I)),l) <> halt SCM+FSA )
assume l < LifeSpan (s1 +* (Initialized I)) ; :: thesis: CurInstr (Computation (s2 +* (Initialized I)),l) <> halt SCM+FSA
then CurInstr (Computation (s1 +* (Initialized I)),l) <> halt SCM+FSA by A11, AMI_1:def 46;
hence CurInstr (Computation (s2 +* (Initialized I)),l) <> halt SCM+FSA by A2, A3, A4, A8, A10, A12, Th38; :: thesis: verum

end;

then for l being Element of NAT st CurInstr (Computation (s2 +* (Initialized I)),l) = halt SCM+FSA holds
LifeSpan (s1 +* (Initialized I)) <= l ;
then A15: LifeSpan (s1 +* (Initialized I)) = LifeSpan (s2 +* (Initialized I)) by A13, A14, AMI_1:def 46;
then A16: Result (s2 +* (Initialized I)) = Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I))) by A13, AMI_1:122;
A17: Result (s1 +* (Initialized I)) = Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I))) by A11, 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 A18: 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 A2, A3, A4, A8, A10, A12, A16, A17, A18, 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 A2, A3, A4, A8, A10, A12, A16, A17, 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 (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A11, AMI_1:122
.= IC (Computation (s2 +* (Initialized I)),(LifeSpan (s2 +* (Initialized I)))) by A2, A3, A4, A8, A10, A12, A15, Th38
.= IC (Result (s2 +* (Initialized I))) by A13, AMI_1:122
.= IC (IExec I,s2) by SCMFSA8A:7 ; :: thesis: verum