let x be set ; :: according to EXTPRO_1:def 13 :: thesis: ( not x in proj1 Sorting-Function or ex b₁ being set st
( x = b₁ & (Initialized Bubble-Sort-Algorithm) +* b₁ is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . b₁ c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* b₁)) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being set st
( x = b₁ & (Initialized Bubble-Sort-Algorithm) +* b₁ is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . b₁ c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* 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 = Initialized Bubble-Sort-Algorithm;
RR: NPP (Initialized Bubble-Sort-Algorithm) = Initialize ((intloc 0) .--> 1) by SCMFSA6A:79;
A2: Bubble-Sort-Algorithm c= Initialized Bubble-Sort-Algorithm by SCMFSA6A:26;
A3: dom d = {(fsloc 0)} by A1, FUNCOP_1:19;
take d ; :: thesis: ( x = d & (Initialized Bubble-Sort-Algorithm) +* d is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* d)) )
thus x = d ; :: thesis: ( (Initialized Bubble-Sort-Algorithm) +* d is Autonomy of Bubble-Sort-Algorithm & Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* d)) )
A4: (Initialized Bubble-Sort-Algorithm) +* d is autonomic by A1, Th68;
A5: dom (Initialized Bubble-Sort-Algorithm) misses dom d by A1, Th46;

now

let t be State of SCM+FSA; :: thesis: ( NPP ((Initialized Bubble-Sort-Algorithm) +* d) c= t implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) c= P holds
P halts_on t )
assume A6: NPP ((Initialized Bubble-Sort-Algorithm) +* d) c= t ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) c= P holds
P halts_on t
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) c= P implies P halts_on t )
assume A7: ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) c= P ; :: thesis: P halts_on t
set bf = bubble-sort (fsloc 0);
A8: Initialized Bubble-Sort-Algorithm c= (Initialized Bubble-Sort-Algorithm) +* d by A5, FUNCT_4:33;
then Initialize ((intloc 0) .--> 1) c= NPP ((Initialized Bubble-Sort-Algorithm) +* d) by RR, COMPOS_1:170;
then A9: Initialize ((intloc 0) .--> 1) c= t by A6, XBOOLE_1:1;
ProgramPart (Initialized Bubble-Sort-Algorithm) c= ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) by A8, RELAT_1:105;
then ProgramPart (Initialized Bubble-Sort-Algorithm) c= P by A7, XBOOLE_1:1;
hence P halts_on t by Lm26, A9, RR, EXTPRO_1:def 10; :: thesis: verum

end;

then A10: (Initialized Bubble-Sort-Algorithm) +* d is halting by EXTPRO_1:def 10;
fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then A11: {(fsloc 0)} c= FinSeq-Locations by ZFMISC_1:37;
A12: dom d misses NAT by A11, A3, SCMFSA_2:14, XBOOLE_1:63;
A13: dom Bubble-Sort-Algorithm c= NAT by RELAT_1:def 18;
A14: ((Initialized Bubble-Sort-Algorithm) +* d) +* Bubble-Sort-Algorithm = (Initialized Bubble-Sort-Algorithm) +* (d +* Bubble-Sort-Algorithm) by FUNCT_4:15
.= (Initialized Bubble-Sort-Algorithm) +* (Bubble-Sort-Algorithm +* d) by A13, A12, FUNCT_4:36, XBOOLE_1:63
.= ((Initialized Bubble-Sort-Algorithm) +* Bubble-Sort-Algorithm) +* d by FUNCT_4:15
.= (Initialized Bubble-Sort-Algorithm) +* d by A2, FUNCT_4:103, FUNCT_4:104 ;
hence A15: (Initialized Bubble-Sort-Algorithm) +* d is Autonomy of Bubble-Sort-Algorithm by A10, A4, EXTPRO_1:def 11; :: thesis: Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* 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: (Initialized Bubble-Sort-Algorithm) +* d c= t by PBOOLE:156;
(Initialize ((intloc 0) .--> 1)) +* d c= (Initialized Bubble-Sort-Algorithm) +* d by RR, FUNCT_4:131;
then C19: (Initialize ((intloc 0) .--> 1)) +* d c= t by A19, XBOOLE_1:1;
B19: ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) c= ProgramPart t by A19, RELAT_1:105;
Bubble-Sort-Algorithm c= (Initialized Bubble-Sort-Algorithm) +* d by A14, FUNCT_4:26;
then Bubble-Sort-Algorithm c= t by A19, XBOOLE_1:1;
then Bubble-Sort-Algorithm c= ProgramPart t by RELAT_1:210;
then 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 ((ProgramPart t),t)) . (fsloc 0) = u by A1, Th67, C19;
A23: u = z by A16, A17, A20, A21, CLASSES1:84, RFINSEQ:36;
fsloc 0 in the carrier of SCM+FSA ;
then A24: fsloc 0 in dom (Result ((ProgramPart t),t)) by PARTFUN1:def 4;
fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then dom d c= FinSeq-Locations by A3, ZFMISC_1:37;
then dom d c= Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_1:10;
then d is data-only by COMPOS_1:31;
then NPP ((Initialized Bubble-Sort-Algorithm) +* d) = (Initialize ((intloc 0) .--> 1)) +* d by RR, COMPOS_1:67;
then d c= NPP ((Initialized Bubble-Sort-Algorithm) +* d) by FUNCT_4:26;
then A25: dom d c= dom (NPP ((Initialized Bubble-Sort-Algorithm) +* d)) by RELAT_1:25;
A26: dom ((fsloc 0) .--> z) = {(fsloc 0)} by FUNCOP_1:19;
A27: dom d misses {(IC )} by A3, SCMFSA_2:82, ZFMISC_1:17;

now

assume dom d meets NAT ; :: thesis: contradiction
then consider x being set such that
A28: x in dom d and
A29: x in NAT by XBOOLE_0:3;
x = fsloc 0 by A28, A3, TARSKI:def 1;
hence contradiction by A29, SCMFSA_2:85; :: thesis: verum

end;

then dom d misses {(IC )} \/ NAT by A27, XBOOLE_1:70;
then d is data-only by COMPOS_1:def 23;
then dom d misses NAT by COMPOS_1:40;
then A30: ProgramPart ((Initialized Bubble-Sort-Algorithm) +* d) = ProgramPart (Initialized Bubble-Sort-Algorithm) by FUNCT_4:76;
Bubble-Sort-Algorithm = ProgramPart (Initialized Bubble-Sort-Algorithm) by SCMFSA6A:33;
then Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* d)) = (Result ((ProgramPart t),t)) | (dom (NPP ((Initialized Bubble-Sort-Algorithm) +* d))) by A19, A15, A30, B19, EXTPRO_1:def 12;
hence Sorting-Function . d c= Result (Bubble-Sort-Algorithm,((Initialized Bubble-Sort-Algorithm) +* d)) by A3, A18, A22, A23, A24, A26, A25, FUNCT_4:90, RELAT_1:186; :: thesis: verum