let P1, P2 be Instruction-Sequence of SCM+FSA; 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; 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; 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; ( 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
; ( 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
; 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;
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))
;
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;
( 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]
;
S2[k + 1]
hence
S1[
Comput (
(P1 +* I),
(Initialize s1),
(k + 1)),
Comput (
(P2 +* I),
(Initialize s2),
(k + 1))]
by A16, A18, A20, Th21;
( 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;
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
;
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))) )
; verum