let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st not I refers 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 not I refers 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: ( not I refers 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: not I refers 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 (0,SCM+FSA)));
set S1 = s1 +* (I +* (Start-At (0,SCM+FSA)));
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 (0,SCM+FSA)))) . b = (s2 +* (I +* (Start-At (0,SCM+FSA)))) . b )
assume A4: a <> b ; :: thesis: (s1 +* (I +* (Start-At (0,SCM+FSA)))) . b = (s2 +* (I +* (Start-At (0,SCM+FSA)))) . b
A5: not b in dom (I +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
not b in dom (I +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
hence (s1 +* (I +* (Start-At (0,SCM+FSA)))) . b = s1 . b by FUNCT_4:12
.= s2 . b by A2, A4
.= (s2 +* (I +* (Start-At (0,SCM+FSA)))) . 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 (0,SCM+FSA)))) . f = (s2 +* (I +* (Start-At (0,SCM+FSA)))) . f
A8: not f in dom (I +* (Start-At (0,SCM+FSA))) by SCMFSA6B:13;
not f in dom (I +* (Start-At (0,SCM+FSA))) by SCMFSA6B:13;
hence (s1 +* (I +* (Start-At (0,SCM+FSA)))) . f = s1 . f by FUNCT_4:12
.= s2 . f by A6
.= (s2 +* (I +* (Start-At (0,SCM+FSA)))) . f by A8, FUNCT_4:12 ;
:: thesis: verum

end;

A9: (I +* (Start-At (0,SCM+FSA))) +* (I +* (Start-At (0,SCM+FSA))) = I +* (Start-At (0,SCM+FSA)) ;
then A10: (s1 +* (I +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA))) = s1 +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:15;
A11: (s2 +* (I +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA))) = s2 +* (I +* (Start-At (0,SCM+FSA))) 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 (0,SCM+FSA))) by A12, A13, Th39;

A15: now

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

end;

ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s1 +* (I +* (Start-At (0,SCM+FSA))) by A13, SCMFSA7B:def 8;
then consider n being Element of NAT such that
A16: CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA by EXTPRO_1:30;
TX1: ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
TX2: ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA by A1, A3, A7, A10, A11, A14, A16, Th38, TX1, TX2;
then ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s2 +* (I +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
hence ( I is_closed_on s2 & I is_halting_on s2 ) by A15, SCMFSA7B:def 7, SCMFSA7B:def 8; :: thesis: verum