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

A3: now

let c be Element of NAT ; :: thesis: ( c < len (aSeq (a,k)) implies s . (0 + c) = (aSeq (a,k)) . c )
assume c < len (aSeq (a,k)) ; :: thesis: s . (0 + c) = (aSeq (a,k)) . c
then c in dom (aSeq (a,k)) by NAT_1:45;
hence s . (0 + c) = (aSeq (a,k)) . c by A2, GRFUNC_1:8; :: thesis: verum

end;

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