let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st not I refersrefer 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 refersrefer 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 refersrefer 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 refersrefer 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 AMI_1:146;
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 AMI_1:146;
hence ( I is_closed_on s2 & I is_halting_on s2 ) by A15, SCMFSA7B:def 7, SCMFSA7B:def 8; :: thesis: verum