set q = Insert-Sort-Algorithm ;
set p = Initialize (() .--> 1);
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in dom Sorting-Function or ex b1 being set st
( x = b1 & (Initialize (() .--> 1)) +* b1 is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b1 c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* b1)) ) )

assume x in dom Sorting-Function ; :: thesis: ex b1 being set st
( x = b1 & (Initialize (() .--> 1)) +* b1 is Autonomy of Insert-Sort-Algorithm & Sorting-Function . b1 c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* b1)) )

then consider w being FinSequence of INT such that
A1: x = () .--> w by SCMFSA_M:35;
reconsider d = x as data-only FinPartState of SCM+FSA by A1;
A2: dom d = {()} by A1;
consider t being State of SCM+FSA such that
A3: (Initialize (() .--> 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 {()} by ;
fsloc 0 <> intloc 0 by SCMFSA_2:58;
then A6: dom d misses {()} by ;
dom (Initialize (() .--> 1)) = (dom (() .--> 1)) \/ {()} by MEMSTR_0:42
.= {()} \/ {()} ;
then A7: dom d misses dom (Initialize (() .--> 1)) by ;
A8: d +* (Initialize (() .--> 1)) = (Initialize (() .--> 1)) +* d by ;
A9: now :: thesis: for t being State of SCM+FSA st (Initialize (() .--> 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 (() .--> 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 (() .--> 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 ();
Initialize (() .--> 1) c= (Initialize (() .--> 1)) +* d by ;
then Initialize (() .--> 1) c= t by ;
hence P halts_on t by ; :: thesis: verum
end;
take d ; :: thesis: ( x = d & (Initialize (() .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* d)) )
thus x = d ; :: thesis: ( (Initialize (() .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm & Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* d)) )
Initialized d = d +* (Initialize (() .--> 1))
.= (Initialize (() .--> 1)) +* d by
.= (Initialize (() .--> 1)) +* d
.= (Initialize (() .--> 1)) +* d ;
then ( (Initialize (() .--> 1)) +* d is Insert-Sort-Algorithm -halted & (Initialize (() .--> 1)) +* d is Insert-Sort-Algorithm -autonomic ) by A1, A9, Th28;
hence A12: (Initialize (() .--> 1)) +* d is Autonomy of Insert-Sort-Algorithm by EXTPRO_1:def 12; :: thesis: Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* d))
fsloc 0 in the carrier of SCM+FSA ;
then A13: fsloc 0 in dom (Result (P,t)) by PARTFUN1:def 2;
(Initialize (() .--> 1)) +* d c= t by A3;
then A14: Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* d)) = (Result (P,t)) | (dom ((Initialize (() .--> 1)) +* d)) by ;
(Initialize (() .--> 1)) +* (() .--> w) c= (Initialize (() .--> 1)) +* d by A1;
then (Initialize (() .--> 1)) +* (() .--> w) c= t by ;
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)) . () = u by ;
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 = () .--> z by ;
d c= (Initialize (() .--> 1)) +* d by FUNCT_4:25;
then A21: dom d c= dom ((Initialize (() .--> 1)) +* d) by RELAT_1:11;
A23: u = z by ;
A24: (fsloc 0) .--> u c= Result (P,t) by ;
dom (() .--> z) c= dom ((Initialize (() .--> 1)) +* d) by ;
then (fsloc 0) .--> z c= (Result (P,t)) | (dom ((Initialize (() .--> 1)) +* d)) by ;
hence Sorting-Function . d c= Result (Insert-Sort-Algorithm,((Initialize (() .--> 1)) +* d)) by ; :: thesis: verum