set q = Insert-Sort-Algorithm ;
set p = Initialized Insert-Sort-Algorithm;
F2: Insert-Sort-Algorithm c= Initialized Insert-Sort-Algorithm by SCMFSA6A:26;
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 Insert-Sort-Algorithm) +* b₁ is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b₁ c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* b₁)) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being set st
( x = b₁ & (Initialized Insert-Sort-Algorithm) +* b₁ is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b₁ c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* b₁)) )
then consider w being FinSequence of INT such that
A1: x = (fsloc 0) .--> w by SCMBSORT:60;
reconsider d = x as FinPartState of SCM+FSA by A1;
consider t being State of SCM+FSA such that
A2: (Initialized Insert-Sort-Algorithm) +* d c= t by PBOOLE:156;
A3: dom (Initialized Insert-Sort-Algorithm) misses dom d by A1, SCMBSORT:46;

A4: now

set bf = insert-sort (fsloc 0);
let t be State of SCM+FSA; :: thesis: ( (Initialized Insert-Sort-Algorithm) +* d c= t implies ProgramPart t halts_on t )
assume A5: (Initialized Insert-Sort-Algorithm) +* d c= t ; :: thesis: ProgramPart t halts_on t
Initialized Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm) +* d by A3, FUNCT_4:33;
then Initialized Insert-Sort-Algorithm c= t by A5, XBOOLE_1:1;
hence ProgramPart t halts_on t by Lm12, EXTPRO_1:def 10; :: thesis: verum

end;

take d ; :: thesis: ( x = d & (Initialized Insert-Sort-Algorithm) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) )
thus x = d ; :: thesis: ( (Initialized Insert-Sort-Algorithm) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) )
d c= (Initialized Insert-Sort-Algorithm) +* d by FUNCT_4:26;
then A7: dom d c= dom ((Initialized Insert-Sort-Algorithm) +* d) by RELAT_1:25;
A10: dom d = {(fsloc 0)} by A1, FUNCOP_1:19;

xx: 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;
x = fsloc 0 by W1, A10, TARSKI:def 1;
hence contradiction by W2, SCMFSA_2:85; :: thesis: verum

end;

fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then X1: {(fsloc 0)} c= FinSeq-Locations by ZFMISC_1:37;
X3: dom Insert-Sort-Algorithm c= NAT by RELAT_1:def 18;
dom d misses NAT by XBOOLE_1:63, X1, A10, SCMFSA_2:14;
then XX: dom d misses dom Insert-Sort-Algorithm by X3, XBOOLE_1:63;
((Initialized Insert-Sort-Algorithm) +* d) +* Insert-Sort-Algorithm = (Initialized Insert-Sort-Algorithm) +* (d +* Insert-Sort-Algorithm) by FUNCT_4:15
.= (Initialized Insert-Sort-Algorithm) +* (Insert-Sort-Algorithm +* d) by XX, FUNCT_4:36
.= ((Initialized Insert-Sort-Algorithm) +* Insert-Sort-Algorithm) +* d by FUNCT_4:15
.= (Initialized Insert-Sort-Algorithm) +* d by F2, FUNCT_4:79 ;
then ( ((Initialized Insert-Sort-Algorithm) +* d) +* Insert-Sort-Algorithm is halting & ((Initialized Insert-Sort-Algorithm) +* d) +* Insert-Sort-Algorithm is autonomic ) by A1, A4, Th48, EXTPRO_1:def 10;
hence LL: (Initialized Insert-Sort-Algorithm) +* d is Autonomy of Insert-Sort-Algorithm by EXTPRO_1:def 11; :: thesis: Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d))
K: dom d misses {(IC SCM+FSA)} by A10, SCMFSA_2:82, ZFMISC_1:17;
dom d misses {(IC SCM+FSA)} \/ NAT by K, XBOOLE_1:70, xx;
then d is data-only by COMPOS_1:def 23;
then dom d misses NAT by COMPOS_1:40;
then NN: ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) = ProgramPart (Initialized Insert-Sort-Algorithm) by FUNCT_4:76;
KK: (Initialized Insert-Sort-Algorithm) +* d is Autonomy of Insert-Sort-Algorithm by LL;
fsloc 0 in the carrier of SCM+FSA ;
then A8: fsloc 0 in dom (Result ((ProgramPart t),t)) by PARTFUN1:def 4;
VV: Insert-Sort-Algorithm = ProgramPart (Initialized Insert-Sort-Algorithm) by SCMFSA8C:25;
A9: Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) = (Result ((ProgramPart t),t)) | (dom ((Initialized Insert-Sort-Algorithm) +* d)) by A2, EXTPRO_1:def 12, KK, VV, NN;
consider u being FinSequence of REAL such that
A11: w,u are_fiberwise_equipotent and
A12: u is non-increasing and
u is FinSequence of INT and
A13: (Result ((ProgramPart t),t)) . (fsloc 0) = u by A1, A2, Th47;
consider z being FinSequence of REAL such that
A14: w,z are_fiberwise_equipotent and
A15: z is non-increasing and
z is FinSequence of INT and
A16: Sorting-Function . d = (fsloc 0) .--> z by A1, SCMBSORT:61;
A17: dom ((fsloc 0) .--> z) = {(fsloc 0)} by FUNCOP_1:19;
u: u = z by A14, A15, A11, A12, CLASSES1:84, RFINSEQ:36;
x1: dom ((fsloc 0) .--> z) c= dom ((Initialized Insert-Sort-Algorithm) +* d) by A1, A7, A17, FUNCOP_1:19;
thus Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) by A16, x1, A9, A13, A8, u, FUNCT_4:90, RELAT_1:186; :: thesis: verum