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