set q = Insert-Sort-Algorithm ;
set p = Initialize ((intloc 0) .--> 1);
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 Sorting-Function or ex b₁ being set st
( x = b₁ & (Initialize ((intloc 0) .--> 1)) +* b₁ is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b₁ c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b₁)) ) )
assume x in dom Sorting-Function ; :: thesis: ex b₁ being set st
( x = b₁ & (Initialize ((intloc 0) .--> 1)) +* b₁ is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b₁ c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* b₁)) )
then consider w being FinSequence of INT such that
A2: x = (fsloc 0) .--> w by SCMBSORT:36;
reconsider d = x as data-only FinPartState of SCM+FSA by A2;
A10: dom d = {(fsloc 0)} by A2, FUNCOP_1:13;
consider t being State of SCM+FSA such that
A3: (Initialize ((intloc 0) .--> 1)) +* d c= t by PBOOLE:141;
consider P being Instruction-Sequence of SCM+FSA such that
B7: Insert-Sort-Algorithm c= P by PBOOLE:145;
fsloc 0 <> IC by SCMFSA_2:57;
then X5: dom d misses {(IC )} by A10, ZFMISC_1:11;
fsloc 0 <> intloc 0 by SCMFSA_2:58;
then X6: dom d misses {(intloc 0)} by A10, ZFMISC_1:11;
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ {(IC )} by MEMSTR_0:42
.= {(IC )} \/ {(intloc 0)} by FUNCOP_1:13 ;
then X1: dom d misses dom (Initialize ((intloc 0) .--> 1)) by X5, X6, XBOOLE_1:70;
UU: d +* (Initialize ((intloc 0) .--> 1)) = (Initialize ((intloc 0) .--> 1)) +* d by X1, FUNCT_4:35;

A5: now

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 Insert-Sort-Algorithm c= P holds
P halts_on t )
assume A6: (Initialize ((intloc 0) .--> 1)) +* d c= t ; :: thesis: for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
P halts_on t
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P implies P halts_on t )
assume A7: Insert-Sort-Algorithm c= P ; :: thesis: P halts_on t
set bf = insert-sort (fsloc 0);
Initialize ((intloc 0) .--> 1) c= (Initialize ((intloc 0) .--> 1)) +* d by UU, FUNCT_4:25;
then Initialize ((intloc 0) .--> 1) c= t by A6, XBOOLE_1:1;
hence P halts_on t by Lm12, A7, SCM_HALT:def 2; :: thesis: verum

end;

take d ; :: thesis: ( x = d & (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) )
thus x = d ; :: thesis: ( (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) )
Initialized d = d +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 3
.= (Initialize ((intloc 0) .--> 1)) +* d by X1, FUNCT_4:35
.= (Initialize ((intloc 0) .--> 1)) +* d
.= (Initialize ((intloc 0) .--> 1)) +* d ;
then ( (Initialize ((intloc 0) .--> 1)) +* d is Insert-Sort-Algorithm -halted & (Initialize ((intloc 0) .--> 1)) +* d is Insert-Sort-Algorithm -autonomic ) by A2, A5, Th48, EXTPRO_1:def 11;
hence A18: (Initialize ((intloc 0) .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm by EXTPRO_1:def 12; :: thesis: Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d))
fsloc 0 in the carrier of SCM+FSA ;
then A22: fsloc 0 in dom (Result (P,t)) by PARTFUN1:def 2;
(Initialize ((intloc 0) .--> 1)) +* d c= t by A3;
then A24: Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) = (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d)) by A18, B7, EXTPRO_1:def 13;
(Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= (Initialize ((intloc 0) .--> 1)) +* d by A2;
then (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= t by A3, XBOOLE_1:1;
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 (P,t)) . (fsloc 0) = u by Th47, B7;
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:37;
d c= (Initialize ((intloc 0) .--> 1)) +* d by FUNCT_4:25;
then A31: dom d c= dom ((Initialize ((intloc 0) .--> 1)) +* d) by RELAT_1:11;
A32: dom ((fsloc 0) .--> z) = {(fsloc 0)} by FUNCOP_1:13;
A33: u = z by A28, A29, A25, A26, CLASSES1:76, RFINSEQ:23;
U1: (fsloc 0) .--> u c= Result (P,t) by A27, A22, FUNCT_4:85;
dom ((fsloc 0) .--> z) c= dom ((Initialize ((intloc 0) .--> 1)) +* d) by A2, A32, A31, FUNCOP_1:13;
then (fsloc 0) .--> z c= (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d)) by U1, A33, RELAT_1:151;
hence Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) by A30, A24; :: thesis: verum