set q = Insert-Sort-Algorithm ;
set p = Initialize ((intloc 0) .--> 1);
let x be set ; EXTPRO_1:def 14 ( not x in dom Sorting-Function or ex b1 being set st
( x = b1 & (Initialize ((intloc 0) .--> 1)) +* b1 is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b1 c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b1)) ) )
assume
x in dom Sorting-Function
; ex b1 being set st
( x = b1 & (Initialize ((intloc 0) .--> 1)) +* b1 is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b1 c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b1)) )
then consider w being FinSequence of INT such that
A1:
x = (fsloc 0) .--> w
by SCMFSA_M:35;
reconsider d = x as data-only FinPartState of SCM+FSA by A1;
A2:
dom d = {(fsloc 0)}
by A1;
consider t being State of SCM+FSA such that
A3:
(Initialize ((intloc 0) .--> 1)) +* d c= t
by PBOOLE:141;
consider P being Instruction-Sequence of SCM+FSA such that
A4:
Insert-Sort-Algorithm c= P
by PBOOLE:145;
fsloc 0 <> IC
by SCMFSA_2:57;
then A5:
dom d misses {(IC )}
by A2, ZFMISC_1:11;
fsloc 0 <> intloc 0
by SCMFSA_2:58;
then A6:
dom d misses {(intloc 0)}
by A2, ZFMISC_1:11;
dom (Initialize ((intloc 0) .--> 1)) =
(dom ((intloc 0) .--> 1)) \/ {(IC )}
by MEMSTR_0:42
.=
{(IC )} \/ {(intloc 0)}
;
then A7:
dom d misses dom (Initialize ((intloc 0) .--> 1))
by A5, A6, XBOOLE_1:70;
A8:
d +* (Initialize ((intloc 0) .--> 1)) = (Initialize ((intloc 0) .--> 1)) +* d
by A7, FUNCT_4:35;
take
d
; ( x = d & (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) )
thus
x = d
; ( (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) )
Initialized d =
d +* (Initialize ((intloc 0) .--> 1))
.=
(Initialize ((intloc 0) .--> 1)) +* d
by A7, FUNCT_4:35
.=
(Initialize ((intloc 0) .--> 1)) +* d
.=
(Initialize ((intloc 0) .--> 1)) +* d
;
then
( (Initialize ((intloc 0) .--> 1)) +* d is Insert-Sort-Algorithm -halted & (Initialize ((intloc 0) .--> 1)) +* d is Insert-Sort-Algorithm -autonomic )
by A1, A9, Th28;
hence A12:
(Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm
by EXTPRO_1:def 12; Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d))
fsloc 0 in the carrier of SCM+FSA
;
then A13:
fsloc 0 in dom (Result (P,t))
by PARTFUN1:def 2;
(Initialize ((intloc 0) .--> 1)) +* d c= t
by A3;
then A14:
Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) = (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d))
by A12, A4, EXTPRO_1:def 13;
(Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= (Initialize ((intloc 0) .--> 1)) +* d
by A1;
then
(Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= t
by A3, XBOOLE_1:1;
then consider u being FinSequence of REAL such that
A15:
w,u are_fiberwise_equipotent
and
A16:
u is non-increasing
and
u is FinSequence of INT
and
A17:
(Result (P,t)) . (fsloc 0) = u
by Th27, A4;
consider z being FinSequence of REAL such that
A18:
w,z are_fiberwise_equipotent
and
A19:
z is non-increasing
and
z is FinSequence of INT
and
A20:
Sorting-Function . d = (fsloc 0) .--> z
by A1, SCMFSA_M:36;
d c= (Initialize ((intloc 0) .--> 1)) +* d
by FUNCT_4:25;
then A21:
dom d c= dom ((Initialize ((intloc 0) .--> 1)) +* d)
by RELAT_1:11;
A23:
u = z
by A18, A19, A15, A16, CLASSES1:76, RFINSEQ:23;
A24:
(fsloc 0) .--> u c= Result (P,t)
by A17, A13, FUNCT_4:85;
dom ((fsloc 0) .--> z) c= dom ((Initialize ((intloc 0) .--> 1)) +* d)
by A1, A21;
then
(fsloc 0) .--> z c= (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d))
by A24, A23, RELAT_1:151;
hence
Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d))
by A20, A14; verum