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 ) holds
for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
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 ) holds
for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
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 ) holds
for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
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 ) implies for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) )
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 for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) )
set S2 = Initialize s2;
set Q2 = P2 +* I;
set S1 = Initialize s1;
set Q1 = P1 +* I;
A2: I c= P1 +* I by FUNCT_4:25;
A3: I c= P2 +* I by FUNCT_4:25;
defpred S1[ State of SCM+FSA, State of SCM+FSA] means ( ( for b being Int-Location st a <> b holds
$1 . b = $2 . b ) & ( for f being FinSeq-Location holds $1 . f = $2 . f ) );
assume that
A4: for b being Int-Location st a <> b holds
s1 . b = s2 . b and
A5: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )
A6: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A7: now :: thesis: for f being FinSeq-Location holds (Initialize s1) . f = (Initialize s2) . f
let f be FinSeq-Location ; :: thesis: (Initialize s1) . f = (Initialize s2) . f
A8: not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
hence (Initialize s1) . f = s1 . f by FUNCT_4:11
.= s2 . f by A5
.= (Initialize s2) . f by A8, FUNCT_4:11 ;
:: thesis: verum
end;
defpred S2[ Nat] means ( S1[ Comput ((P1 +* I),(Initialize s1),$1), Comput ((P2 +* I),(Initialize s2),$1)] & IC (Comput ((P1 +* I),(Initialize s1),$1)) = IC (Comput ((P2 +* I),(Initialize s2),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),$1))) );
A9: IC (Comput ((P1 +* I),(Initialize s1),0)) = IC (Initialize s1)
.= IC (Start-At (0,SCM+FSA)) by A6, FUNCT_4:13
.= IC (Initialize s2) by A6, FUNCT_4:13
.= IC (Comput ((P2 +* I),(Initialize s2),0)) ;
A10: now :: thesis: for b being Int-Location st a <> b holds
(Initialize s1) . b = (Initialize s2) . b
let b be Int-Location; :: thesis: ( a <> b implies (Initialize s1) . b = (Initialize s2) . b )
assume A11: a <> b ; :: thesis: (Initialize s1) . b = (Initialize s2) . b
A12: not b in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialize s1) . b = s1 . b by FUNCT_4:11
.= s2 . b by A4, A11
.= (Initialize s2) . b by A12, FUNCT_4:11 ;
:: thesis: verum
end;
IC (Initialize s1) = 0 by MEMSTR_0:def 11;
then A13: IC (Initialize s1) in dom I by AFINSQ_1:65;
then A14: IC (Comput ((P1 +* I),(Initialize s1),0)) in dom I ;
A15: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A16: Comput ((P1 +* I),(Initialize s1),(k + 1)) = Following ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k)))),(Comput ((P1 +* I),(Initialize s1),k))) ;
A17: IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A2, A13, AMISTD_1:21;
A18: Comput ((P2 +* I),(Initialize s2),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k)))),(Comput ((P2 +* I),(Initialize s2),k))) ;
A19: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),k))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),k))) by PBOOLE:143;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = I . (IC (Comput ((P1 +* I),(Initialize s1),k))) by A17, A19, A2, GRFUNC_1:2;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) in rng I by A17, FUNCT_1:def 3;
then A20: not CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) refers a by A1, SCMFSA7B:def 2;
assume A21: S2[k] ; :: thesis: S2[k + 1]
hence S1[ Comput ((P1 +* I),(Initialize s1),(k + 1)), Comput ((P2 +* I),(Initialize s2),(k + 1))] by A16, A18, A20, Th21; :: thesis: ( IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* I),(Initialize s2),(k + 1))) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(k + 1)))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1)))) )
thus A22: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* I),(Initialize s2),(k + 1))) by A21, A16, A18, A20, Th21; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(k + 1)))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1))))
A23: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) in dom I by A2, A13, AMISTD_1:21;
A24: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by PBOOLE:143;
A25: (P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) by PBOOLE:143;
thus CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(k + 1)))) = I . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by A23, A24, A2, GRFUNC_1:2
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1)))) by A22, A23, A25, A3, GRFUNC_1:2 ; :: thesis: verum
end;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),0))) by PBOOLE:143
.= I . (IC (Comput ((P1 +* I),(Initialize s1),0))) by A14, A2, GRFUNC_1:2
.= (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),0))) by A9, A14, A3, GRFUNC_1:2
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),0))) by PBOOLE:143 ;
then A26: S2[ 0 ] by A10, A7, A9;
for k being Nat holds S2[k] from NAT_1:sch 2(A26, A15);
 hence for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) ) ; :: thesis: verum