set DD = {(intloc 0),(IC ),(fsloc 0)};
let w be FinSequence of INT ; (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w) is autonomic
set p = (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w);
set q = Insert-Sort-Algorithm ;
not fsloc 0 in NAT
by SCMFSA10:4;
then
ProgramPart ((fsloc 0) .--> w) = {}
by FUNCOP_1:91;
then A1: ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) =
(ProgramPart (Initialized Insert-Sort-Algorithm)) +* {}
by FUNCT_4:75
.=
ProgramPart (Initialized Insert-Sort-Algorithm)
by FUNCT_4:22
.=
Insert-Sort-Algorithm
by SCMFSA6A:33
;
A2:
(Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w) is 0 -started
by SCMBSORT:47;
set UD = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)};
set Us = (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm);
A3:
UsedIntLoc Insert-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by Th38;
A4:
UsedInt*Loc Insert-Sort-Algorithm = {(fsloc 0)}
by Th39;
then A5:
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by A3, ENUMSET1:62;
A6:
for i being Element of NAT
for s1, s2 being State of SCM+FSA
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT st 11 <= i & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
proof
let i be
Element of
NAT ;
for s1, s2 being State of SCM+FSA
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT st 11 <= i & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc 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 the Instructions of SCM+FSA -valued ManySortedSet of NAT st 11 <= i & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )let P1,
P2 be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
( 11 <= i & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 implies ( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) )
assume that A7:
11
<= i
and A8:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1
and A9:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2
and A10:
Insert-Sort-Algorithm c= P1
and A11:
Insert-Sort-Algorithm c= P2
;
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
A12:
s1 . (intloc 0) =
1
by A8, Lm54
.=
s2 . (intloc 0)
by A9, Lm54
;
A13:
s2 is
0 -started
by A9, A2, COMPOS_1:8;
set Cs11 =
Comput (
P1,
s1,11);
set Cs21 =
Comput (
P2,
s2,11);
A14:
s1 is
0 -started
by A8, A2, COMPOS_1:8;
A15:
s1 . (fsloc 0) =
w
by A8, Lm54
.=
s2 . (fsloc 0)
by A9, Lm54
;
A16:
now let x be
set ;
( x in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) implies (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1 )assume
x in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1then A17:
x in {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by A4, A3, ENUMSET1:62;
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 A17, ENUMSET1:def 6;
suppose A18:
x = fsloc 0
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (fsloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A15, A18, Lm2, A11
;
verum end; suppose A19:
x = intloc 0
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A19, Lm2, A11
;
verum end; suppose A20:
x = intloc 1
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
len (s1 . (fsloc 0))
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A15, A20, Lm2, A11
;
verum end; suppose A21:
x = intloc 2
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A21, Lm2, A11
;
verum end; suppose A22:
x = intloc 3
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A22, Lm2, A11
;
verum end; suppose A23:
x = intloc 4
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A23, Lm2, A11
;
verum end; suppose A24:
x = intloc 5
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A24, Lm2, A11
;
verum end; suppose A25:
x = intloc 6
;
(Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1hence (Comput (P1,s1,11)) . x =
s1 . (intloc 0)
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . x
by A13, A12, A25, Lm2, A11
;
verum end; end;
A26:
for
i being
Element of
NAT holds
IC (Comput (P2,s2,i)) in dom Insert-Sort-Algorithm
by A9, Th46, A11;
A27:
for
i being
Element of
NAT holds
IC (Comput (P1,s1,i)) in dom Insert-Sort-Algorithm
by A8, Th46, A10;
A28:
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P2,s2,11))
by SCMBSORT:56;
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P1,s1,11))
by SCMBSORT:56;
then A29:
(Comput (P1,s1,11)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,11)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm))
by A28, A16, FUNCT_1:165;
(Comput (P1,s1,11)) . (IC ) =
11
by A14, Lm2, A10
.=
(Comput (P2,s2,11)) . (IC )
by A13, Lm2, A11
;
hence
(
(Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) &
(Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
by A7, A29, A27, A26, A10, A11, SCMBSORT:26;
verum
end;
A30:
for s1, s2 being State of SCM+FSA
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being Element of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being Element of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((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 the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
for i being Element of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((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
Element of
NAT ;
( NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((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 A31:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1
and A32:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2
and A33:
Insert-Sort-Algorithm c= P1
and A34:
Insert-Sort-Algorithm c= P2
and A35:
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) )
A36:
s2 is
0 -started
by A32, A2, COMPOS_1:8;
A37:
s1 . (fsloc 0) =
w
by A31, Lm54
.=
s2 . (fsloc 0)
by A32, Lm54
;
A38:
s1 . (intloc 0) =
1
by A31, Lm54
.=
s2 . (intloc 0)
by A32, Lm54
;
A39:
Comput (
P1,
s1,
0)
= s1
by EXTPRO_1:3;
A40:
s1 is
0 -started
by A31, A2, COMPOS_1:8;
then A41:
IC s1 =
0
by COMPOS_1:def 16
.=
IC s2
by A36, COMPOS_1:def 16
;
per cases
( 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 )
by A35, NAT_1:35;
suppose A42:
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 A39, A38, EXTPRO_1:3;
( (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 A39, A41, A42, EXTPRO_1:3;
(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 A39, A37, A42, EXTPRO_1:3;
verum end; suppose A43:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A43, Lm2, A34
;
( (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 A40, A43, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A43, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A43, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A43, Lm2, A34
;
verum end; suppose A44:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A44, Lm2, A34
;
( (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 A40, A44, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A44, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A44, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A44, Lm2, A34
;
verum end; suppose A45:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A45, Lm2, A34
;
( (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 A40, A45, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A45, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A45, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A45, Lm2, A34
;
verum end; suppose A46:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A46, Lm2, A34
;
( (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 A40, A46, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A46, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A46, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A46, Lm2, A34
;
verum end; suppose A47:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A47, Lm2, A34
;
( (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 A40, A47, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A47, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A47, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A47, Lm2, A34
;
verum end; suppose A48:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A48, Lm2, A34
;
( (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 A40, A48, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A48, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A48, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A48, Lm2, A34
;
verum end; suppose A49:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A49, Lm2, A34
;
( (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 A40, A49, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A49, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A49, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A49, Lm2, A34
;
verum end; suppose A50:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A50, Lm2, A34
;
( (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 A40, A50, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A50, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A50, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A50, Lm2, A34
;
verum end; suppose A51:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A51, Lm2, A34
;
( (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 A40, A51, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A51, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A51, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A51, Lm2, A34
;
verum end; suppose A52:
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 A40, Lm2, A33
.=
(Comput (P2,s2,i)) . (intloc 0)
by A36, A38, A52, Lm2, A34
;
( (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 A40, A52, Lm2, A33
.=
(Comput (P2,s2,i)) . (IC )
by A36, A52, Lm2, A34
;
(Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)thus (Comput (P1,s1,i)) . (fsloc 0) =
s1 . (fsloc 0)
by A40, A52, Lm2, A33
.=
(Comput (P2,s2,i)) . (fsloc 0)
by A36, A37, A52, Lm2, A34
;
verum end;
end;
A53:
dom ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (dom Insert-Sort-Algorithm) \/ {(intloc 0),(IC ),(fsloc 0)}
by SCMBSORT:42;
fsloc 0 in FinSeq-Locations
by SCMFSA_2:10;
then A54:
fsloc 0 in Data-Locations SCM+FSA
by SCMFSA_2:127, XBOOLE_0:def 3;
intloc 0 in Int-Locations
by SCMFSA_2:9;
then A55:
intloc 0 in Data-Locations SCM+FSA
by SCMFSA_2:127, XBOOLE_0:def 3;
A56: dom (DataPart ((fsloc 0) .--> w)) =
(dom ((fsloc 0) .--> w)) /\ (Data-Locations SCM+FSA)
by RELAT_1:90
.=
{(fsloc 0)} /\ (Data-Locations SCM+FSA)
by FUNCOP_1:19
.=
{(fsloc 0)}
by A54, ZFMISC_1:52
;
A57:
Data-Locations SCM+FSA misses NAT
by COMPOS_1:51;
dom Insert-Sort-Algorithm c= NAT
by RELAT_1:def 18;
then A58:
Data-Locations SCM+FSA misses dom Insert-Sort-Algorithm
by A57, XBOOLE_1:63;
Initialized Insert-Sort-Algorithm =
Insert-Sort-Algorithm +* (Initialize ((intloc 0) .--> 1))
by SCMFSA6A:def 4
.=
Initialize (Insert-Sort-Algorithm +* ((intloc 0) .--> 1))
by FUNCT_4:15
;
then DataPart (Initialized Insert-Sort-Algorithm) =
((Insert-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA)) +* (DataPart (Start-At (0,SCM+FSA)))
by FUNCT_4:75
.=
((Insert-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA)) +* {}
by COMPOS_1:30
.=
(Insert-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA)
by FUNCT_4:22
.=
(DataPart Insert-Sort-Algorithm) +* (((intloc 0) .--> 1) | (Data-Locations SCM+FSA))
by FUNCT_4:75
.=
{} +* (((intloc 0) .--> 1) | (Data-Locations SCM+FSA))
by A58, RELAT_1:95
.=
((intloc 0) .--> 1) | (Data-Locations SCM+FSA)
by FUNCT_4:21
;
then A59: dom (DataPart (Initialized Insert-Sort-Algorithm)) =
(dom ((intloc 0) .--> 1)) /\ (Data-Locations SCM+FSA)
by RELAT_1:90
.=
{(intloc 0)} /\ (Data-Locations SCM+FSA)
by FUNCOP_1:19
.=
{(intloc 0)}
by A55, ZFMISC_1:52
;
DataPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (DataPart (Initialized Insert-Sort-Algorithm)) +* (DataPart ((fsloc 0) .--> w))
by FUNCT_4:75;
then A60: dom (DataPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))) =
{(fsloc 0)} \/ {(intloc 0)}
by A56, A59, FUNCT_4:def 1
.=
{(intloc 0),(fsloc 0)}
by ENUMSET1:41
;
IC in {(intloc 0),(IC ),(fsloc 0)}
by ENUMSET1:def 1;
then
IC in dom ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))
by A53, XBOOLE_0:def 3;
then A61: dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))) =
{(IC )} \/ (dom (DataPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
by COMPOS_1:70
.=
{(IC ),(intloc 0),(fsloc 0)}
by A60, ENUMSET1:42
.=
{(intloc 0),(IC ),(fsloc 0)}
by ENUMSET1:99
;
for P, Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q holds
for s1, s2 being State of SCM+FSA st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
proof
let P1,
P2 be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
( ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P1 & ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P2 implies for s1, s2 being State of SCM+FSA st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) )
assume that A64:
ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P1
and A65:
ProgramPart ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P2
;
for s1, s2 being State of SCM+FSA st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
let s1,
s2 be
State of
SCM+FSA;
( NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 implies for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) )
assume that A62:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1
and A63:
NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2
;
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
let i be
Element of
NAT ;
(Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
set Cs1i =
Comput (
P1,
s1,
i);
set Cs2i =
Comput (
P2,
s2,
i);
A66:
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P1,s1,i))
by SCMBSORT:56;
A67:
fsloc 0 in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)
by A5, ENUMSET1:def 6;
A68:
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P2,s2,i))
by SCMBSORT:56;
A69:
(
i > 10 implies 10
+ 1
< i + 1 )
by XREAL_1:8;
A70:
intloc 0 in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)
by A5, ENUMSET1:def 6;
A71:
now let x be
set ;
( x in {(intloc 0),(IC ),(fsloc 0)} implies (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1 )assume A72:
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 A72, ENUMSET1:def 1;
suppose A73:
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)) . b1hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A30, A62, A63, A73, A64, A65, A1;
verum end; suppose
i > 10
;
(Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1then
11
<= i
by A69, NAT_1:13;
then
(Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm))
by A6, A62, A63, A64, A65, A1;
hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A70, A66, A68, A73, FUNCT_1:165;
verum end; suppose A74:
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)) . b1hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A30, A62, A63, A74, A64, A65, A1;
verum end; suppose
i > 10
;
(Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1then
11
<= i
by A69, NAT_1:13;
hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A6, A62, A63, A74, A64, A65, A1;
verum end; suppose A75:
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)) . b1hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A30, A62, A63, A75, A64, A65, A1;
verum end; suppose
i > 10
;
(Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1then
11
<= i
by A69, NAT_1:13;
then
(Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm))
by A6, A62, A63, A64, A65, A1;
hence
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
by A67, A66, A68, A75, FUNCT_1:165;
verum end; end;
A76:
{(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P2,s2,i))
by SCMBSORT:55;
{(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P1,s1,i))
by SCMBSORT:55;
then
(Comput (P1,s1,i)) | {(intloc 0),(IC ),(fsloc 0)} = (Comput (P2,s2,i)) | {(intloc 0),(IC ),(fsloc 0)}
by A76, A71, FUNCT_1:165;
hence
(Comput (P1,s1,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (P2,s2,i)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w))))
by A61;
verum
end;
hence
(Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w) is autonomic
by EXTPRO_1:def 9; verum