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