set IS = Insert-Sort-Algorithm ;
set Ii = Initialized Insert-Sort-Algorithm ;
let i be Element of NAT ; :: thesis: for s being State of SCM+FSA
for w being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s holds
IC (Computation s,i) in dom Insert-Sort-Algorithm
let s be State of SCM+FSA ; :: thesis: for w being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s holds
IC (Computation s,i) in dom Insert-Sort-Algorithm
let w be FinSequence of INT ; :: thesis: ( (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s implies IC (Computation s,i) in dom Insert-Sort-Algorithm )
set x = (fsloc 0 ) .--> w;
assume A1: (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s ; :: thesis: IC (Computation s,i) in dom Insert-Sort-Algorithm
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 A2: Initialized Insert-Sort-Algorithm c= s by A1, XBOOLE_1:1;
Insert-Sort-Algorithm is InitHalting Program of SCM+FSA by Th44;
hence IC (Computation s,i) in dom Insert-Sort-Algorithm by A2, SCM_HALT:def 1; :: thesis: verum