let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )
let I be Program of SCM+FSA ; :: thesis: for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )
let a be Int-Location ; :: thesis: ( I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 implies ( I is_closed_on s2 & I is_halting_on s2 ) )
assume A1: I does_not_refer a ; :: thesis: ( ex b being Int-Location st
( a <> b & not s1 . b = s2 . b ) or ex f being FinSeq-Location st not s1 . f = s2 . f or not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
assume A2: for b being Int-Location st a <> b holds
s1 . b = s2 . b ; :: thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )

A3: now

let b be Int-Location ; :: thesis: ( a <> b implies (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b )
assume A4: a <> b ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b
A5: not b in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
not b in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . b = s1 . b by FUNCT_4:12
.= s2 . b by A2, A4
.= (s2 +* (I +* (Start-At (insloc 0 )))) . b by A5, FUNCT_4:12 ;
:: thesis: verum

end;

assume A6: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )

A7: now

let f be FinSeq-Location ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . f = (s2 +* (I +* (Start-At (insloc 0 )))) . f
A8: not f in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:13;
not f in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:13;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . f = s1 . f by FUNCT_4:12
.= s2 . f by A6
.= (s2 +* (I +* (Start-At (insloc 0 )))) . f by A8, FUNCT_4:12 ;
:: thesis: verum

end;

A9: (I +* (Start-At (insloc 0 ))) +* (I +* (Start-At (insloc 0 ))) = I +* (Start-At (insloc 0 )) ;
then A10: (s1 +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) = s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:15;
A11: (s2 +* (I +* (Start-At (insloc 0 )))) +* (I +* (Start-At (insloc 0 ))) = s2 +* (I +* (Start-At (insloc 0 ))) by A9, FUNCT_4:15;
assume that
A12: I is_closed_on s1 and
A13: I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
A14: I is_closed_on s1 +* (I +* (Start-At (insloc 0 ))) by A12, A13, Th39;

A15: now

let k be Element of NAT ; :: thesis: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I
IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A12, SCMFSA7B:def 7;
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A1, A3, A7, A10, A11, A14, Th38; :: thesis: verum

end;

s1 +* (I +* (Start-At (insloc 0 ))) is halting by A13, SCMFSA7B:def 8;
then consider n being Element of NAT such that
A16: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),n) = halt SCM+FSA by AMI_1:def 20;
CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),n) = halt SCM+FSA by A1, A3, A7, A10, A11, A14, A16, Th38;
then s2 +* (I +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence ( I is_closed_on s2 & I is_halting_on s2 ) by A15, SCMFSA7B:def 7, SCMFSA7B:def 8; :: thesis: verum