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 ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_halting_on Initialized s1,P1 holds
( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
let s1, s2 be State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_halting_on Initialized s1,P1 holds
( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
let I be really-closed Program of SCM+FSA; :: thesis: for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_halting_on Initialized s1,P1 holds
( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
let a be Int-Location; :: thesis: ( ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not I refers a & I is_halting_on Initialized s1,P1 implies ( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) ) )
assume that
A1: for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d and
A2: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: ( I refers a or not I is_halting_on Initialized s1,P1 or ( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) ) )
A3: now :: thesis: for d being Int-Location st a <> d holds
(Initialized s1) . d = (Initialized s2) . d
let d be Int-Location; :: thesis: ( a <> d implies (Initialized s1) . b1 = (Initialized s2) . b1 )
assume A4: a <> d ; :: thesis: (Initialized s1) . b1 = (Initialized s2) . b1
per cases ( d = intloc 0 or d <> intloc 0 ) ;
suppose A5: d = intloc 0 ; :: thesis: (Initialized s1) . b1 = (Initialized s2) . b1
hence (Initialized s1) . d = 1 by SCMFSA_M:9
.= (Initialized s2) . d by A5, SCMFSA_M:9 ;
:: thesis: verum
end;
suppose d <> intloc 0 ; :: thesis: (Initialized s1) . b1 = (Initialized s2) . b1
then A6: d is read-write ;
hence (Initialized s1) . d = s1 . d by SCMFSA_M:37
.= s2 . d by A1, A4, A6
.= (Initialized s2) . d by A6, SCMFSA_M:37 ;
:: thesis: verum
end;
end;
end;
set S1 = Initialized s1;
set Q1 = P1 +* I;
set S2 = Initialized s2;
set Q2 = P2 +* I;
assume A7: not I refers a ; :: thesis: ( not I is_halting_on Initialized s1,P1 or ( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) ) )
A8: Initialized s2 = Initialize (Initialized s2) by MEMSTR_0:44;
assume A9: I is_halting_on Initialized s1,P1 ; :: thesis: ( ( for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
A10: now :: thesis: for f being FinSeq-Location holds (Initialized s1) . f = (Initialized s2) . f
let f be FinSeq-Location ; :: thesis: (Initialized s1) . f = (Initialized s2) . f
thus (Initialized s1) . f = s1 . f by SCMFSA_M:37
.= s2 . f by A2
.= (Initialized s2) . f by SCMFSA_M:37 ; :: thesis: verum
end;
then I is_halting_on Initialized s2,P2 by A7, A9, A3, Th24;
then A11: P2 +* I halts_on Initialized s2 by A8, SCMFSA7B:def 7;
A12: Initialized s1 = Initialize (Initialized s1) by MEMSTR_0:44;
then A13: P1 +* I halts_on Initialized s1 by A9, SCMFSA7B:def 7;
now :: thesis: for l being Nat st l < LifeSpan ((P1 +* I),(Initialized s1)) holds
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) <> halt SCM+FSA
let l be Nat; :: thesis: ( l < LifeSpan ((P1 +* I),(Initialized s1)) implies CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) <> halt SCM+FSA )
assume l < LifeSpan ((P1 +* I),(Initialized s1)) ; :: thesis: CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) <> halt SCM+FSA
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),l))) <> halt SCM+FSA by A13, EXTPRO_1:def 15;
hence CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) <> halt SCM+FSA by A7, A3, A10, A12, A8, Th22; :: thesis: verum
end;
then A14: for l being Nat st CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) = halt SCM+FSA holds
LifeSpan ((P1 +* I),(Initialized s1)) <= l ;
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))) = CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))) by A7, A3, A10, A12, A8, Th22
.= halt SCM+FSA by A13, EXTPRO_1:def 15 ;
then A15: LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2)) by A11, A14, EXTPRO_1:def 15;
then A16: Result ((P2 +* I),(Initialized s2)) = Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))) by A11, EXTPRO_1:23;
A17: Result ((P1 +* I),(Initialized s1)) = Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))) by A13, EXTPRO_1:23;
A18: Result ((P1 +* I),(Initialized s1)) = IExec (I,P1,s1) by Th20;
A19: Result ((P2 +* I),(Initialized s2)) = IExec (I,P2,s2) by Th20;
thus for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d by A19, A18, A7, A3, A10, A12, A8, A16, A17, Th22; :: thesis: ( ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
thus for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f by A19, A18, A7, A3, A10, A12, A8, A16, A17, Th22; :: thesis: IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2))
thus IC (IExec (I,P1,s1)) = IC (Result ((P1 +* I),(Initialized s1))) by SCMFSA6B:def 1
.= IC (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1))))) by A13, EXTPRO_1:23
.= IC (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P2 +* I),(Initialized s2))))) by A7, A3, A10, A12, A8, A15, Th22
.= IC (Result ((P2 +* I),(Initialized s2))) by A11, EXTPRO_1:23
.= IC (IExec (I,P2,s2)) by SCMFSA6B:def 1 ; :: thesis: verum