let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 Sorting-Function or ex b₁ being set st
( x = b₁ & (Initialize ((intloc 0) .--> 1)) +* b₁ is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . b₁ c= Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b₁)) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being set st
( x = b₁ & (Initialize ((intloc 0) .--> 1)) +* b₁ is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . b₁ c= Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b₁)) )
then consider w being FinSequence of INT such that
A1: x = (fsloc 0) .--> w by Th60;
reconsider d = x as FinPartState of SCM+FSA by A1;
set q = Bubble-Sort-Algorithm ;
set p = Initialize ((intloc 0) .--> 1);
A3: dom d = {(fsloc 0)} by A1, FUNCOP_1:13;
take d ; :: thesis: ( 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 ; :: thesis: ( (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) )
X5: dom d misses {(IC )} by A3, SCMFSA_2:57, ZFMISC_1:11;
X6: dom d misses {(intloc 0)} by A3, SCMFSA_2:58, ZFMISC_1:11;
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ {(IC )} by MEMSTR_0:42
.= {(IC )} \/ {(intloc 0)} by FUNCOP_1:13 ;
then X1: dom d misses dom (Initialize ((intloc 0) .--> 1)) by X5, X6, XBOOLE_1:70;
UU: d +* (Initialize ((intloc 0) .--> 1)) = (Initialize ((intloc 0) .--> 1)) +* d by X1, FUNCT_4:35;
Initialized d = d +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 3
.= (Initialize ((intloc 0) .--> 1)) +* d by X1, FUNCT_4:35
.= (Initialize ((intloc 0) .--> 1)) +* d
.= (Initialize ((intloc 0) .--> 1)) +* d ;
then A4: (Initialize ((intloc 0) .--> 1)) +* d is Bubble-Sort-Algorithm -autonomic by A1, Th68;

now

let t be State of SCM+FSA; :: thesis: ( (Initialize ((intloc 0) .--> 1)) +* d c= t implies for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
P halts_on t )
assume A6: (Initialize ((intloc 0) .--> 1)) +* d c= t ; :: thesis: for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
P halts_on t
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Bubble-Sort-Algorithm c= P implies P halts_on t )
assume A7: Bubble-Sort-Algorithm c= P ; :: thesis: P halts_on t
set bf = bubble-sort (fsloc 0);
Initialize ((intloc 0) .--> 1) c= (Initialize ((intloc 0) .--> 1)) +* d by UU, FUNCT_4:25;
then Initialize ((intloc 0) .--> 1) c= t by A6, XBOOLE_1:1;
hence P halts_on t by Lm26, A7, SCM_HALT:def 2; :: thesis: verum

end;

then A10: (Initialize ((intloc 0) .--> 1)) +* d is Bubble-Sort-Algorithm -halted by EXTPRO_1:def 11;
thus A15: (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Bubble-Sort-Algorithm by A10, A4, EXTPRO_1:def 12; :: thesis: Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d))
consider z being FinSequence of REAL such that
A16: w,z are_fiberwise_equipotent and
A17: z is non-increasing and
z is FinSequence of INT and
A18: Sorting-Function . d = (fsloc 0) .--> z by A1, Th61;
consider t being State of SCM+FSA such that
A19: (Initialize ((intloc 0) .--> 1)) +* d c= t by PBOOLE:141;
consider T being Instruction-Sequence of SCM+FSA such that
B19: Bubble-Sort-Algorithm c= T by PBOOLE:145;
consider u being FinSequence of REAL such that
A20: w,u are_fiberwise_equipotent and
A21: u is non-increasing and
u is FinSequence of INT and
A22: (Result (T,t)) . (fsloc 0) = u by Th67, A1, A19, B19;
A23: u = z by A16, A17, A20, A21, CLASSES1:76, RFINSEQ:23;
fsloc 0 in the carrier of SCM+FSA ;
then A24: fsloc 0 in dom (Result (T,t)) by PARTFUN1:def 2;
d c= (Initialize ((intloc 0) .--> 1)) +* d by FUNCT_4:25;
then A25: dom d c= dom ((Initialize ((intloc 0) .--> 1)) +* d) by RELAT_1:11;
A26: dom ((fsloc 0) .--> z) = {(fsloc 0)} by FUNCOP_1:13;
Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) = (Result (T,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d)) by A15, A19, B19, EXTPRO_1:def 13;
hence Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) by A3, A18, A22, A23, A24, A26, A25, FUNCT_4:85, RELAT_1:151; :: thesis: verum