let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being 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_closed_on s1,P1 holds
for k being Element of 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 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_closed_on s1,P1 holds
for k being Element of 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 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_closed_on s1,P1 holds
for k being Element of 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 ) & I is_closed_on s1,P1 implies for k being Element of 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 A2: 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_closed_on s1,P1 or for k being Element of 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;
A3: I c= P1 +* I by FUNCT_4:25;
A4: 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
A5: for b being Int-Location st a <> b holds
s1 . b = s2 . b and
A6: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: ( not I is_closed_on s1,P1 or for k being Element of 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))) ) )
B7: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A8: now
let f be FinSeq-Location ; :: thesis: (Initialize s1) . f = (Initialize s2) . f
B9: 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 A6
.= (Initialize s2) . f by B9, FUNCT_4:11 ;
:: thesis: verum
end;
A10: Comput ((P2 +* I),(Initialize s2),0) = Initialize s2 by EXTPRO_1:2;
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))) );
A11: IC (Comput ((P1 +* I),(Initialize s1),0)) = IC (Initialize s1) by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by B7, FUNCT_4:13
.= IC (Initialize s2) by B7, FUNCT_4:13
.= IC (Comput ((P2 +* I),(Initialize s2),0)) by EXTPRO_1:2 ;
A12: now
let b be Int-Location ; :: thesis: ( a <> b implies (Initialize s1) . b = (Initialize s2) . b )
assume A13: a <> b ; :: thesis: (Initialize s1) . b = (Initialize s2) . b
B14: 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 A5, A13
.= (Initialize s2) . b by B14, FUNCT_4:11 ;
:: thesis: verum
end;
A15: Comput ((P1 +* I),(Initialize s1),0) = Initialize s1 by EXTPRO_1:2;
assume A16: I is_closed_on s1,P1 ; :: thesis: for k being Element of 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))) )
A17: IC (Comput ((P1 +* I),(Initialize s1),0)) in dom I by A16, SCMFSA7B:def 6;
A18: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
A19: 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))) ;
A20: IC (Comput ((P1 +* I),(Initialize s1),k)) in dom I by A16, SCMFSA7B:def 6;
A21: 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))) ;
A22: (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 A20, A22, A3, GRFUNC_1:2;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) in rng I by A20, FUNCT_1:def 3;
then A23: not CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) refers a by A2, SCMFSA7B:def 2;
assume A24: S2[k] ; :: thesis: S2[k + 1]
hence S1[ Comput ((P1 +* I),(Initialize s1),(k + 1)), Comput ((P2 +* I),(Initialize s2),(k + 1))] by A19, A21, A23, Th37; :: 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 A25: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* I),(Initialize s2),(k + 1))) by A24, A19, A21, A23, Th37; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),(k + 1)))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1))))
A26: IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) in dom I by A16, SCMFSA7B:def 6;
A27: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by PBOOLE:143;
A28: (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 A26, A27, A3, GRFUNC_1:2
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1)))) by A25, A26, A28, A4, 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 A17, A3, GRFUNC_1:2
.= (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),0))) by A11, A17, A4, GRFUNC_1:2
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),0))) by PBOOLE:143 ;
then A29: S2[ 0 ] by A12, A8, A15, A10, A11;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A29, A18);
 hence for k being Element of 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