set q = Insert-Sort-Algorithm ;
set p = Initialized Insert-Sort-Algorithm;
A1: 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
A2: x = (fsloc 0) .--> w by SCMBSORT:60;
reconsider d = x as FinPartState of SCM+FSA by A2;
consider t being State of SCM+FSA such that
A3: (Initialized Insert-Sort-Algorithm) +* d c= t by PBOOLE:156;
B3: ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) c= ProgramPart t by A3, RELAT_1:105;
A4: dom (Initialized Insert-Sort-Algorithm) misses dom d by A2, SCMBSORT:46;

A5: now

set bf = insert-sort (fsloc 0);
let t be State of SCM+FSA; :: thesis: ( NPP ((Initialized Insert-Sort-Algorithm) +* d) c= t implies for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) c= P holds
P halts_on t )
assume A6: NPP ((Initialized Insert-Sort-Algorithm) +* d) c= t ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Insert-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 Insert-Sort-Algorithm) +* d) c= P implies P halts_on t )
assume A7: ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) c= P ; :: thesis: P halts_on t
A8: Initialized Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm) +* d by A4, FUNCT_4:33;
then NPP (Initialized Insert-Sort-Algorithm) c= NPP ((Initialized Insert-Sort-Algorithm) +* d) by COMPOS_1:170;
then A9: NPP (Initialized Insert-Sort-Algorithm) c= t by A6, XBOOLE_1:1;
ProgramPart (Initialized Insert-Sort-Algorithm) c= ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) by A8, RELAT_1:105;
then ProgramPart (Initialized Insert-Sort-Algorithm) c= P by A7, XBOOLE_1:1;
hence P halts_on t by Lm12, A9, 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)) )
A10: dom d = {(fsloc 0)} by A2, FUNCOP_1:19;

A11: now

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

end;

fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then A14: {(fsloc 0)} c= FinSeq-Locations by ZFMISC_1:37;
A15: dom Insert-Sort-Algorithm c= NAT by RELAT_1:def 18;
dom d misses NAT by A14, A10, SCMFSA_2:14, XBOOLE_1:63;
then A16: dom d misses dom Insert-Sort-Algorithm by A15, XBOOLE_1:63;
A17: ((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 A16, FUNCT_4:36
.= ((Initialized Insert-Sort-Algorithm) +* Insert-Sort-Algorithm) +* d by FUNCT_4:15
.= (Initialized Insert-Sort-Algorithm) +* d by A1, FUNCT_4:104 ;
then ( ((Initialized Insert-Sort-Algorithm) +* d) +* Insert-Sort-Algorithm is halting & ((Initialized Insert-Sort-Algorithm) +* d) +* Insert-Sort-Algorithm is autonomic ) by A2, A5, Th48, EXTPRO_1:def 10;
hence A18: (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))
A19: dom d misses {(IC )} by A10, SCMFSA_2:82, ZFMISC_1:17;
dom d misses {(IC )} \/ NAT by A19, A11, XBOOLE_1:70;
then d is data-only by COMPOS_1:def 23;
then dom d misses NAT by COMPOS_1:40;
then A20: ProgramPart ((Initialized Insert-Sort-Algorithm) +* d) = ProgramPart (Initialized Insert-Sort-Algorithm) by FUNCT_4:76;
A21: (Initialized Insert-Sort-Algorithm) +* d is Autonomy of Insert-Sort-Algorithm by A18;
fsloc 0 in the carrier of SCM+FSA ;
then A22: fsloc 0 in dom (Result ((ProgramPart t),t)) by PARTFUN1:def 4;
A23: Insert-Sort-Algorithm = ProgramPart (Initialized Insert-Sort-Algorithm) by SCMFSA6A:33;
A24: Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) = (Result ((ProgramPart t),t)) | (dom (NPP ((Initialized Insert-Sort-Algorithm) +* d))) by A3, A21, A23, A20, B3, EXTPRO_1:def 12;
Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm) +* d by A17, FUNCT_4:26;
then Insert-Sort-Algorithm c= t by A3, XBOOLE_1:1;
then Insert-Sort-Algorithm c= ProgramPart t by RELAT_1:210;
then consider u being FinSequence of REAL such that
A25: w,u are_fiberwise_equipotent and
A26: u is non-increasing and
u is FinSequence of INT and
A27: (Result ((ProgramPart t),t)) . (fsloc 0) = u by A2, A3, Th47;
consider z being FinSequence of REAL such that
A28: w,z are_fiberwise_equipotent and
A29: z is non-increasing and
z is FinSequence of INT and
A30: Sorting-Function . d = (fsloc 0) .--> z by A2, SCMBSORT:61;
fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then dom d c= FinSeq-Locations by A10, 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 Insert-Sort-Algorithm) +* d) = (NPP (Initialized Insert-Sort-Algorithm)) +* d by COMPOS_1:67;
then d c= NPP ((Initialized Insert-Sort-Algorithm) +* d) by FUNCT_4:26;
then A31: dom d c= dom (NPP ((Initialized Insert-Sort-Algorithm) +* d)) by RELAT_1:25;
A32: dom ((fsloc 0) .--> z) = {(fsloc 0)} by FUNCOP_1:19;
A33: u = z by A28, A29, A25, A26, CLASSES1:84, RFINSEQ:36;
dom ((fsloc 0) .--> z) c= dom (NPP ((Initialized Insert-Sort-Algorithm) +* d)) by A2, A32, A31, FUNCOP_1:19;
hence Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialized Insert-Sort-Algorithm) +* d)) by A30, A24, A27, A22, A33, FUNCT_4:90, RELAT_1:186; :: thesis: verum