let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being State of SCM+FSA
for I being really-closed 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_halting_on s1,P1 holds
I is_halting_on s2,P2
let s1, s2 be State of SCM+FSA; for I being really-closed 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_halting_on s1,P1 holds
I is_halting_on s2,P2
let I be really-closed 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_halting_on s1,P1 holds
I is_halting_on s2,P2
let a be Int-Location; ( 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_halting_on s1,P1 implies I is_halting_on s2,P2 )
assume A1:
not I refers a
; ( 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_halting_on s1,P1 or I is_halting_on s2,P2 )
set S2 = Initialize s2;
set Q2 = P2 +* I;
set S1 = Initialize s1;
set Q1 = P1 +* I;
assume A2:
for b being Int-Location st a <> b holds
s1 . b = s2 . b
; ( ex f being FinSeq-Location st not s1 . f = s2 . f or not I is_halting_on s1,P1 or I is_halting_on s2,P2 )
assume A3:
for f being FinSeq-Location holds s1 . f = s2 . f
; ( not I is_halting_on s1,P1 or I is_halting_on s2,P2 )
assume A4:
I is_halting_on s1,P1
; I is_halting_on s2,P2
P1 +* I halts_on Initialize s1
by A4, SCMFSA7B:def 7;
then consider n being Nat such that
A5:
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),n))) = halt SCM+FSA
;
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),n))) = halt SCM+FSA
by A1, A5, Th22, A3, A2;
then
P2 +* I halts_on Initialize s2
by EXTPRO_1:29;
hence
I is_halting_on s2,P2
by SCMFSA7B:def 7; verum