let i be Element of NAT ; :: thesis: for s being State of SCM+FSA
for w being FinSequence of INT
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s & Insert-Sort-Algorithm c= P holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let s be State of SCM+FSA; :: thesis: for w being FinSequence of INT
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s & Insert-Sort-Algorithm c= P holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let w be FinSequence of INT ; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s & Insert-Sort-Algorithm c= P holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s & Insert-Sort-Algorithm c= P implies IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )
set IS = Insert-Sort-Algorithm ;
set Ii = Initialized Insert-Sort-Algorithm;
set x = (fsloc 0) .--> w;
dom (Initialized Insert-Sort-Algorithm) misses dom ((fsloc 0) .--> w) by SCMBSORT:46;
then Initialized Insert-Sort-Algorithm c= (Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w) by FUNCT_4:33;
then B1: NPP (Initialized Insert-Sort-Algorithm) c= NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) by COMPOS_1:170;
assume NPP ((Initialized Insert-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s ; :: thesis: ( not Insert-Sort-Algorithm c= P or IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )
then A2: NPP (Initialized Insert-Sort-Algorithm) c= s by B1, XBOOLE_1:1;
assume A3: Insert-Sort-Algorithm c= P ; :: thesis: IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
E: NPP (Initialized Insert-Sort-Algorithm) = Initialize ((intloc 0) .--> 1) by SCMFSA6A:79;
Insert-Sort-Algorithm is InitHalting by Th44;
then IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm by A3, A2, E, SCM_HALT:def 1;
hence IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm ; :: thesis: verum