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 dom 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
A1: x = (fsloc 0) .--> w by SCMFSA_M:35;
reconsider d = x as data-only FinPartState of SCM+FSA by A1;
A2: dom d = {(fsloc 0)} by A1;
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
A4: Insert-Sort-Algorithm c= P by PBOOLE:145;
fsloc 0 <> IC by SCMFSA_2:57;
then A5: dom d misses {(IC )} by A2, ZFMISC_1:11;
fsloc 0 <> intloc 0 by SCMFSA_2:58;
then A6: dom d misses {(intloc 0)} by A2, ZFMISC_1:11;
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ {(IC )} by MEMSTR_0:42
.= {(IC )} \/ {(intloc 0)} ;
then A7: dom d misses dom (Initialize ((intloc 0) .--> 1)) by A5, A6, XBOOLE_1:70;
A8: d +* (Initialize ((intloc 0) .--> 1)) = (Initialize ((intloc 0) .--> 1)) +* d by A7, FUNCT_4:35;

A9: now :: thesis: for t being State of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* d c= t holds
for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
P halts_on t

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 A10: (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 A11: 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 A8, FUNCT_4:25;
then Initialize ((intloc 0) .--> 1) c= t by A10, XBOOLE_1:1;
hence P halts_on t by Lm12, A11, 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))
.= (Initialize ((intloc 0) .--> 1)) +* d by A7, 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 A1, A9, Th28;
hence A12: (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 A13: fsloc 0 in dom (Result (P,t)) by PARTFUN1:def 2;
(Initialize ((intloc 0) .--> 1)) +* d c= t by A3;
then A14: Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) = (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d)) by A12, A4, EXTPRO_1:def 13;
(Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= (Initialize ((intloc 0) .--> 1)) +* d by A1;
then (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> w) c= t by A3, XBOOLE_1:1;
then consider u being FinSequence of REAL such that
A15: w,u are_fiberwise_equipotent and
A16: u is non-increasing and
u is FinSequence of INT and
A17: (Result (P,t)) . (fsloc 0) = u by Th27, A4;
consider z being FinSequence of REAL such that
A18: w,z are_fiberwise_equipotent and
A19: z is non-increasing and
z is FinSequence of INT and
A20: Sorting-Function . d = (fsloc 0) .--> z by A1, SCMFSA_M:36;
d c= (Initialize ((intloc 0) .--> 1)) +* d by FUNCT_4:25;
then A21: dom d c= dom ((Initialize ((intloc 0) .--> 1)) +* d) by RELAT_1:11;
A23: u = z by A18, A19, A15, A16, CLASSES1:76, RFINSEQ:23;
A24: (fsloc 0) .--> u c= Result (P,t) by A17, A13, FUNCT_4:85;
dom ((fsloc 0) .--> z) c= dom ((Initialize ((intloc 0) .--> 1)) +* d) by A1, A21;
then (fsloc 0) .--> z c= (Result (P,t)) | (dom ((Initialize ((intloc 0) .--> 1)) +* d)) by A24, A23, RELAT_1:151;
hence Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize ((intloc 0) .--> 1)) +* d)) by A20, A14; :: thesis: verum