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: for c being Element of NAT st c < len (aSeq (a,k)) holds
P . (0 + c) = (aSeq (a,k)) . c by ;
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 ;
hence IC (Comput (P,s,i)) = i ; :: thesis: verum