set Ba = Insert-Sort-Algorithm ;
let i be Nat; for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let P be Instruction-Sequence of SCM+FSA; ( Insert-Sort-Algorithm c= P implies for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )
assume A1:
Insert-Sort-Algorithm c= P
; for w being FinSequence of INT st Initialized ((fsloc 0) .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
let w be FinSequence of INT ; ( Initialized ((fsloc 0) .--> w) c= s implies IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )
set x = (fsloc 0) .--> w;
assume A2:
Initialized ((fsloc 0) .--> w) c= s
; IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
set BSA = Bubble-Sort-Algorithm ;
Initialize ((intloc 0) .--> 1) c= Initialized ((fsloc 0) .--> w)
by FUNCT_4:25;
then
Initialize ((intloc 0) .--> 1) c= s
by A2, XBOOLE_1:1;
then
IC s = 0
by MEMSTR_0:47;
then
IC s in dom Insert-Sort-Algorithm
by AFINSQ_1:65;
hence
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
by A1, AMISTD_1:21; verum