let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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:26;
A4: I c= P2 +* I by FUNCT_4:26;
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 COMPOS_1:52;
A8: now
let f be FinSeq-Location ; :: thesis: (Initialize s1) . f = (Initialize s2) . f
Start-At (0,SCM+FSA) c= Initialize I by FUNCT_4:26;
then dom (Start-At (0,SCM+FSA)) c= dom (Initialize I) by RELAT_1:25;
then B9: not f in dom (Start-At (0,SCM+FSA)) by SCMFSA6B:13;
hence (Initialize s1) . f = s1 . f by FUNCT_4:12
.= s2 . f by A6
.= (Initialize s2) . f by B9, FUNCT_4:12 ;
:: thesis: verum
end;
A10: Comput ((P2 +* I),(Initialize s2),0) = Initialize s2 by EXTPRO_1:3;
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:3
.= IC (Start-At (0,SCM+FSA)) by B7, FUNCT_4:14
.= IC (Initialize s2) by B7, FUNCT_4:14
.= IC (Comput ((P2 +* I),(Initialize s2),0)) by EXTPRO_1:3 ;
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
Start-At (0,SCM+FSA) c= Initialize I by FUNCT_4:26;
then dom (Start-At (0,SCM+FSA)) c= dom (Initialize I) by RELAT_1:25;
then B14: not b in dom (Start-At (0,SCM+FSA)) by SCMFSA6B:12;
hence (Initialize s1) . b = s1 . b by FUNCT_4:12
.= s2 . b by A5, A13
.= (Initialize s2) . b by B14, FUNCT_4:12 ;
:: thesis: verum
end;
A15: Comput ((P1 +* I),(Initialize s1),0) = Initialize s1 by EXTPRO_1:3;
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 7;
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:4
.= 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 7;
A21: Comput ((P2 +* I),(Initialize s2),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) by EXTPRO_1:4
.= 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:158;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = I . (IC (Comput ((P1 +* I),(Initialize s1),k))) by A20, A22, A3, GRFUNC_1:8;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) in rng I by A20, FUNCT_1:def 5;
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 7;
A27: (P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) by PBOOLE:158;
A28: (P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) by PBOOLE:158;
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:8
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),(k + 1)))) by A25, A26, A28, A4, GRFUNC_1:8 ; :: thesis: verum
end;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),0))) by PBOOLE:158
.= I . (IC (Comput ((P1 +* I),(Initialize s1),0))) by A17, A3, GRFUNC_1:8
.= (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),0))) by A11, A17, A4, GRFUNC_1:8
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),0))) by PBOOLE:158 ;
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