let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( 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 ; :: thesis: 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 ; :: 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)) )
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;
now :: thesis: for t being State of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* d c= t holds
for P being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P holds
P halts_on t
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 A8: (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 A9: 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 A6, FUNCT_4:25;
then Initialize ((intloc 0) .--> 1) c= t by A8, XBOOLE_1:1;
hence P halts_on t by Lm26, A9, SCM_HALT:def 2; :: thesis: verum
end;
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; :: thesis: 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; :: thesis: verum