let s be 0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st aSeq (a,k) c= P holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i
let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for k being Integer st aSeq (a,k) c= P holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i
let a be Int-Location ; :: thesis: for k being Integer st aSeq (a,k) c= P holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i
let k be Integer; :: thesis: ( aSeq (a,k) c= P implies for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i )
assume A1: aSeq (a,k) c= P ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = i

A2: now

let c be Element of NAT ; :: thesis: ( c < len (aSeq (a,k)) implies P . (0 + c) = (aSeq (a,k)) . c )
assume c < len (aSeq (a,k)) ; :: thesis: P . (0 + c) = (aSeq (a,k)) . c
then c in dom (aSeq (a,k)) by NAT_1:44;
hence P . (0 + c) = (aSeq (a,k)) . c by A1, GRFUNC_1:2; :: thesis: verum

end;

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (a,k)) implies IC (Comput (P,s,i)) = i )
assume i <= len (aSeq (a,k)) ; :: thesis: IC (Comput (P,s,i)) = i
then IC (Comput (P,s,i)) = 0 + i by A2, Lm3;
hence IC (Comput (P,s,i)) = i ; :: thesis: verum