set Ba = Insert-Sort-Algorithm ;
let i be Nat; :: thesis: 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 (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm

let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P implies for w being FinSequence of INT st Initialized (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )

assume A1: Insert-Sort-Algorithm c= P ; :: thesis: for w being FinSequence of INT st Initialized (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm

let w be FinSequence of INT ; :: thesis: ( Initialized (() .--> w) c= s implies IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm )
set x = () .--> w;
assume A2: Initialized (() .--> w) c= s ; :: thesis: IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
set BSA = Bubble-Sort-Algorithm ;
Initialize (() .--> 1) c= Initialized (() .--> w) by FUNCT_4:25;
then Initialize (() .--> 1) c= s by ;
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 ; :: thesis: verum