let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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; :: 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_halting_on s1,P1 holds
I is_halting_on s2,P2
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_halting_on s1,P1 implies I is_halting_on s2,P2 )
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_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 ; :: thesis: ( 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 ; :: thesis: ( not I is_halting_on s1,P1 or I is_halting_on s2,P2 )
assume A4: I is_halting_on s1,P1 ; :: thesis: 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; :: thesis: verum