let x be set ; :: according to AMI_1:def 30 :: thesis: ( not x in proj1 Sorting-Function or ex b₁ being set st
( x = b₁ & ((ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm )) +* b₁ is set & Sorting-Function . b₁ c= Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* b₁) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being set st
( x = b₁ & ((ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm )) +* b₁ is set & Sorting-Function . b₁ c= Result (ProgramPart (Initialized 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 p = Initialized Bubble-Sort-Algorithm ;
F1: (ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm ) = Initialized Bubble-Sort-Algorithm by FUNCT_4:119;
A2: dom d = {(fsloc 0 )} by A1, FUNCOP_1:19;
take d ; :: thesis: ( x = d & ((ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm )) +* d is set & Sorting-Function . d c= Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* d) )
thus x = d ; :: thesis: ( ((ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm )) +* d is set & Sorting-Function . d c= Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* d) )
A3: (Initialized Bubble-Sort-Algorithm ) +* d is autonomic by A1, Th68;
A4: dom (Initialized Bubble-Sort-Algorithm ) misses dom d by A1, Th46;

now

let t be State of SCM+FSA ; :: thesis: ( (Initialized Bubble-Sort-Algorithm ) +* d c= t implies ProgramPart t halts_on t )
assume A6: (Initialized Bubble-Sort-Algorithm ) +* d c= t ; :: thesis: ProgramPart t halts_on t
set bf = bubble-sort (fsloc 0 );
Initialized Bubble-Sort-Algorithm c= (Initialized Bubble-Sort-Algorithm ) +* d by A4, FUNCT_4:33;
then Initialized Bubble-Sort-Algorithm c= t by A6, XBOOLE_1:1;
hence ProgramPart t halts_on t by Lm26, AMI_1:def 26; :: thesis: verum

end;

then A7: (Initialized Bubble-Sort-Algorithm ) +* d is halting by AMI_1:def 26;
(Initialized Bubble-Sort-Algorithm ) +* d is autonomic by A1, Th68;
hence ((ProgramPart (Initialized Bubble-Sort-Algorithm )) +* (Initialized Bubble-Sort-Algorithm )) +* d is pre-program of SCM+FSA by A7, F1; :: thesis: Sorting-Function . d c= Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* d)
consider z being FinSequence of REAL such that
A8: w,z are_fiberwise_equipotent and
A9: z is non-increasing and
z is FinSequence of INT and
A10: Sorting-Function . d = (fsloc 0 ) .--> z by A1, Th61;
consider t being State of SCM+FSA such that
A11: (Initialized Bubble-Sort-Algorithm ) +* d c= t by PBOOLE:156;
consider u being FinSequence of REAL such that
A12: w,u are_fiberwise_equipotent and
A13: u is non-increasing and
u is FinSequence of INT and
A14: (Result (ProgramPart t),t) . (fsloc 0 ) = u by A1, A11, Th67;
A15: u = z by A8, A9, A12, A13, CLASSES1:84, RFINSEQ:36;
fsloc 0 in the carrier of SCM+FSA ;
then A16: fsloc 0 in dom (Result (ProgramPart t),t) by PARTFUN1:def 4;
d c= (Initialized Bubble-Sort-Algorithm ) +* d by FUNCT_4:26;
then A17: dom d c= dom ((Initialized Bubble-Sort-Algorithm ) +* d) by RELAT_1:25;
A18: dom ((fsloc 0 ) .--> z) = {(fsloc 0 )} by FUNCOP_1:19;
fsloc 0 <> IC SCM+FSA by SCMFSA_2:82;
then K: dom d misses {(IC SCM+FSA )} by A2, ZFMISC_1:17;

now

assume dom d meets NAT ; :: thesis: contradiction
then consider x being set such that
W1: x in dom d and
W2: x in NAT by XBOOLE_0:3;
A: x is Element of NAT by W2;
x = fsloc 0 by W1, A2, TARSKI:def 1;
hence contradiction by A, SCMFSA_2:85; :: thesis: verum

end;

then dom d misses {(IC SCM+FSA )} \/ NAT by K, XBOOLE_1:70;
then d is data-only by COMPOS_1:def 23;
then dom d misses NAT by COMPOS_1:40;
then V: ProgramPart ((Initialized Bubble-Sort-Algorithm ) +* d) = ProgramPart (Initialized Bubble-Sort-Algorithm ) by FUNCT_4:76;
Result (ProgramPart ((Initialized Bubble-Sort-Algorithm ) +* d)),((Initialized Bubble-Sort-Algorithm ) +* d) = (Result (ProgramPart t),t) | (dom ((Initialized Bubble-Sort-Algorithm ) +* d)) by A3, A7, A11, AMI_1:def 29;
then A83: Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* d) = (Result (ProgramPart t),t) | (dom ((Initialized Bubble-Sort-Algorithm ) +* d)) by V;
Sorting-Function . d c= (Result (ProgramPart t),t) | (dom ((Initialized Bubble-Sort-Algorithm ) +* d)) by A2, A10, A14, A15, A16, A17, A18, F1, FUNCT_4:90, RELAT_1:186;
hence Sorting-Function . d c= Result (ProgramPart (Initialized Bubble-Sort-Algorithm )),((Initialized Bubble-Sort-Algorithm ) +* d) by A83; :: thesis: verum