let w be FinSequence of INT ; Initialized ((fsloc 0) .--> w) is Bubble-Sort-Algorithm -autonomic
set p = Initialized ((fsloc 0) .--> w);
set q = Bubble-Sort-Algorithm ;
A1:
for P, Q being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q holds
for s1, s2 being State of SCM+FSA
for i being Nat st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
proof
let P,
Q be
Instruction-Sequence of
SCM+FSA;
( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q implies for s1, s2 being State of SCM+FSA
for i being Nat st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) ) )
assume A2:
(
Bubble-Sort-Algorithm c= P &
Bubble-Sort-Algorithm c= Q )
;
for s1, s2 being State of SCM+FSA
for i being Nat st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
let s1,
s2 be
State of
SCM+FSA;
for i being Nat st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )let i be
Nat;
( Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 implies ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) ) )
assume that A3:
Initialized ((fsloc 0) .--> w) c= s1
and A4:
Initialized ((fsloc 0) .--> w) c= s2
and A5:
i <= 10
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
A6:
Bubble-Sort-Algorithm c= P
by A2;
A7:
Bubble-Sort-Algorithm c= Q
by A2;
A8:
s1 is
0 -started
by A3, MEMSTR_0:17;
A9:
s2 is
0 -started
by A4, MEMSTR_0:17;
A10:
s1 . (intloc 0) =
1
by A3, SCMFSA_M:33
.=
s2 . (intloc 0)
by A4, SCMFSA_M:33
;
A11:
s1 . (fsloc 0) =
w
by A3, SCMFSA_M:33
.=
s2 . (fsloc 0)
by A4, SCMFSA_M:33
;
A12:
IC s1 =
0
by A8
.=
IC s2
by A9
;
not not
i = 0 & ... & not
i = 10
by A5;
per cases then
( i = 0 or i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 )
;
suppose A13:
i = 0
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence
(Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0)
by A10;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus
(Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC )
by A12, A13;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
by A11, A13;
verum end; suppose A14:
i = 1
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A14, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
1
by A2, A8, A14, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A7, A9, A14, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A6, A8, A14, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A14, Lm21
;
verum end; suppose A15:
i = 2
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A6, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A15, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
2
by A2, A8, A15, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A15, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A15, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A15, Lm21
;
verum end; suppose A16:
i = 3
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A16, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
3
by A2, A8, A16, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A16, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A6, A8, A16, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A16, Lm21
;
verum end; suppose A17:
i = 4
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A6, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A17, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
4
by A2, A8, A17, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A17, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A17, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A17, Lm21
;
verum end; suppose A18:
i = 5
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A6, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A18, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
5
by A2, A8, A18, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A18, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A18, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A18, Lm21
;
verum end; suppose A19:
i = 6
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A19, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
6
by A2, A8, A19, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A19, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A19, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A19, Lm21
;
verum end; suppose A20:
i = 7
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A6, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A20, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
7
by A2, A8, A20, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A20, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A20, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A20, Lm21
;
verum end; suppose A21:
i = 8
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A21, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
8
by A2, A8, A21, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A21, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A21, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A21, Lm21
;
verum end; suppose A22:
i = 9
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A22, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
9
by A2, A8, A22, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A22, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A22, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A22, Lm21
;
verum end; suppose A23:
i = 10
;
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )hence (Comput (P,s1,i)) . (intloc 0) =
s1 . (intloc 0)
by A2, A8, Lm21
.=
(Comput (Q,s2,i)) . (intloc 0)
by A2, A9, A10, A23, Lm21
;
( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )thus (Comput (P,s1,i)) . (IC ) =
10
by A2, A8, A23, Lm21
.=
(Comput (Q,s2,i)) . (IC )
by A2, A9, A23, Lm21
;
(Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)thus (Comput (P,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A2, A8, A23, Lm21
.=
(Comput (Q,s2,i)) . (fsloc 0)
by A2, A9, A11, A23, Lm21
;
verum end; end;
end;
set UD = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)};
set Us = (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm);
A24:
UsedI*Loc Bubble-Sort-Algorithm = {(fsloc 0)}
by Th22;
A25:
UsedILoc Bubble-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by Th21;
then A26:
(UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by A24, ENUMSET1:22;
A27:
for P, Q being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q holds
for i being Nat
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
proof
let P,
Q be
Instruction-Sequence of
SCM+FSA;
( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q implies for i being Nat
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) ) )
assume A28:
(
Bubble-Sort-Algorithm c= P &
Bubble-Sort-Algorithm c= Q )
;
for i being Nat
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
let i be
Nat;
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )let s1,
s2 be
State of
SCM+FSA;
( 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 implies ( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) ) )
assume that A29:
11
<= i
and A30:
Initialized ((fsloc 0) .--> w) c= s1
and A31:
Initialized ((fsloc 0) .--> w) c= s2
;
( (Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
set Cs11 =
Comput (
P,
s1,11);
set Cs21 =
Comput (
Q,
s2,11);
A32:
s1 is
0 -started
by A30, MEMSTR_0:17;
A33:
s2 is
0 -started
by A31, MEMSTR_0:17;
A34:
s1 . (intloc 0) =
1
by A30, SCMFSA_M:33
.=
s2 . (intloc 0)
by A31, SCMFSA_M:33
;
A35:
s1 . (fsloc 0) =
w
by A30, SCMFSA_M:33
.=
s2 . (fsloc 0)
by A31, SCMFSA_M:33
;
A36:
(UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,11))
by Th19;
A37:
(UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,11))
by Th19;
now for x being set st x in (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) holds
(Comput (P,s1,11)) . x = (Comput (Q,s2,11)) . xlet x be
set ;
( x in (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) implies (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1 )assume
x in (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1then A38:
x in {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by A24, A25, ENUMSET1:22;
per cases
( x = fsloc 0 or x = intloc 0 or x = intloc 1 or x = intloc 2 or x = intloc 3 or x = intloc 4 or x = intloc 5 or x = intloc 6 )
by A38, ENUMSET1:def 6;
suppose A39:
x = fsloc 0
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (fsloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A35, A39, Lm21
;
verum end; suppose A40:
x = intloc 0
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A40, Lm21
;
verum end; suppose A41:
x = intloc 1
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
len (s1 . (fsloc 0))
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A35, A41, Lm21
;
verum end; suppose A42:
x = intloc 2
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A42, Lm21
;
verum end; suppose A43:
x = intloc 3
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A43, Lm21
;
verum end; suppose A44:
x = intloc 4
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A44, Lm21
;
verum end; suppose A45:
x = intloc 5
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A45, Lm21
;
verum end; suppose A46:
x = intloc 6
;
(Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1hence (Comput (P,s1,11)) . x =
s1 . (intloc 0)
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . x
by A33, A28, A34, A46, Lm21
;
verum end; end; end;
then A47:
(Comput (P,s1,11)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,11)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm))
by A36, A37, FUNCT_1:95;
A48:
(Comput (P,s1,11)) . (IC ) =
11
by A32, A28, Lm21
.=
(Comput (Q,s2,11)) . (IC )
by A33, A28, Lm21
;
A49:
for
i being
Nat holds
IC (Comput (P,s1,i)) in dom Bubble-Sort-Algorithm
by A30, Th27, A28;
for
i being
Nat holds
IC (Comput (Q,s2,i)) in dom Bubble-Sort-Algorithm
by A31, Th27, A28;
hence
(
(Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) &
(Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
by A29, A47, A48, A49, Th14, A28;
verum
end;
set DD = {(intloc 0),(IC ),(fsloc 0)};
let P, Q be Instruction-Sequence of SCM+FSA; EXTPRO_1:def 10 ( not Bubble-Sort-Algorithm c= P or not Bubble-Sort-Algorithm c= Q or for b1, b2 being set holds
( not Initialized ((fsloc 0) .--> w) c= b1 or not Initialized ((fsloc 0) .--> w) c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,b2,b3)) | (dom (Initialized ((fsloc 0) .--> w))) ) )
assume A50:
( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q )
; for b1, b2 being set holds
( not Initialized ((fsloc 0) .--> w) c= b1 or not Initialized ((fsloc 0) .--> w) c= b2 or for b3 being set holds (Comput (P,b1,b3)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,b2,b3)) | (dom (Initialized ((fsloc 0) .--> w))) )
let s1, s2 be State of SCM+FSA; ( not Initialized ((fsloc 0) .--> w) c= s1 or not Initialized ((fsloc 0) .--> w) c= s2 or for b1 being set holds (Comput (P,s1,b1)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,b1)) | (dom (Initialized ((fsloc 0) .--> w))) )
assume that
A51:
Initialized ((fsloc 0) .--> w) c= s1
and
A52:
Initialized ((fsloc 0) .--> w) c= s2
; for b1 being set holds (Comput (P,s1,b1)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,b1)) | (dom (Initialized ((fsloc 0) .--> w)))
let i be Nat; (Comput (P,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
reconsider i = i as Nat ;
set Cs1i = Comput (P,s1,i);
set Cs2i = Comput (Q,s2,i);
A53:
dom (Initialized ((fsloc 0) .--> w)) = {(intloc 0),(IC ),(fsloc 0)}
by SCMFSA_M:31;
A54:
{(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P,s1,i))
by SCMFSA_M:34;
A55:
{(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (Q,s2,i))
by SCMFSA_M:34;
A56:
intloc 0 in (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)
by A26, ENUMSET1:def 6;
A57:
fsloc 0 in (UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)
by A26, ENUMSET1:def 6;
A58:
(UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,i))
by Th19;
A59:
(UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,i))
by Th19;
A60:
( i > 10 implies 10 + 1 < i + 1 )
by XREAL_1:6;
now for x being set st x in {(intloc 0),(IC ),(fsloc 0)} holds
(Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . xlet x be
set ;
( x in {(intloc 0),(IC ),(fsloc 0)} implies (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1 )assume A61:
x in {(intloc 0),(IC ),(fsloc 0)}
;
(Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1per cases
( x = intloc 0 or x = IC or x = fsloc 0 )
by A61, ENUMSET1:def 1;
suppose A62:
x = intloc 0
;
(Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1per cases
( i <= 10 or i > 10 )
;
suppose
i > 10
;
(Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1then
11
<= i
by A60, NAT_1:13;
then
(Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm))
by A27, A51, A52, A50;
hence
(Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x
by A56, A58, A59, A62, FUNCT_1:95;
verum end; end; end; suppose A64:
x = fsloc 0
;
(Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1per cases
( i <= 10 or i > 10 )
;
suppose
i > 10
;
(Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1then
11
<= i
by A60, NAT_1:13;
then
(Comput (P,s1,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedI*Loc Bubble-Sort-Algorithm) \/ (UsedILoc Bubble-Sort-Algorithm))
by A27, A51, A52, A50;
hence
(Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x
by A57, A58, A59, A64, FUNCT_1:95;
verum end; end; end; end; end;
hence
(Comput (P,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
by A53, A54, A55, FUNCT_1:95; verum