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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) )
A1: ProgramPart I = I by RELAT_1:209;
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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) )
set S2 = s2 +* (Initialize I);
set Q2 = P2 +* I;
set S1 = s1 +* (Initialize I);
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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) )
A7: IC in dom (Initialize I) by COMPOS_1:141;
A8: now
let f be FinSeq-Location ; :: thesis: (s1 +* (Initialize I)) . f = (s2 +* (Initialize I)) . f
A9: not f in dom (Initialize I) by SCMFSA6B:13;
hence (s1 +* (Initialize I)) . f = s1 . f by FUNCT_4:12
.= s2 . f by A6
.= (s2 +* (Initialize I)) . f by A9, FUNCT_4:12 ;
:: thesis: verum
end;
A10: Comput ((P2 +* I),(s2 +* (Initialize I)),0) = s2 +* (Initialize I) by EXTPRO_1:3;
defpred S2[ Nat] means ( S1[ Comput ((P1 +* I),(s1 +* (Initialize I)),$1), Comput ((P2 +* I),(s2 +* (Initialize I)),$1)] & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),$1)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),$1))) );
A11: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0)) = (s1 +* (Initialize I)) . (IC ) by EXTPRO_1:3
.= (Initialize I) . (IC ) by A7, FUNCT_4:14
.= (s2 +* (Initialize I)) . (IC ) by A7, FUNCT_4:14
.= IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0)) by EXTPRO_1:3 ;
A12: now
let b be Int-Location ; :: thesis: ( a <> b implies (s1 +* (Initialize I)) . b = (s2 +* (Initialize I)) . b )
assume A13: a <> b ; :: thesis: (s1 +* (Initialize I)) . b = (s2 +* (Initialize I)) . b
A14: not b in dom (Initialize I) by SCMFSA6B:12;
hence (s1 +* (Initialize I)) . b = s1 . b by FUNCT_4:12
.= s2 . b by A5, A13
.= (s2 +* (Initialize I)) . b by A14, FUNCT_4:12 ;
:: thesis: verum
end;
A15: Comput ((P1 +* I),(s1 +* (Initialize I)),0) = s1 +* (Initialize I) 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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )
A17: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0)) in dom I by A16, SCMFSA7B:def 7, A1;
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),(s1 +* (Initialize I)),(k + 1)) = Following ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k)))),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) ;
A20: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) in dom I by A16, SCMFSA7B:def 7, A1;
A21: Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k)))),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ;
A22: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by PBOOLE:158;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = I . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by A20, A22, GRFUNC_1:8, A3;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) in rng I by A20, FUNCT_1:def 5;
then A23: not CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) refers a by A2, SCMFSA7B:def 2;
assume A24: S2[k] ; :: thesis: S2[k + 1]
hence S1[ Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)), Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))] by A19, A21, A23, Th37; :: thesis: ( IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) )
thus A25: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))) by A24, A19, A21, A23, Th37; :: thesis: CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))))
A26: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) in dom I by A16, SCMFSA7B:def 7, A1;
A27: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
A28: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
thus CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = I . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by A26, A27, GRFUNC_1:8, A3
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by A25, A26, A28, GRFUNC_1:8, A4 ; :: thesis: verum
end;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) by PBOOLE:158
.= I . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) by A17, GRFUNC_1:8, A3
.= (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0))) by A11, A17, GRFUNC_1:8, A4
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),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),(s1 +* (Initialize I)),k)) . b = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f ) & IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ) ; :: thesis: verum