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 A1, AFINSQ_1:86, GRFUNC_1:2;
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