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

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