let s be State of SCM+FSA ; :: thesis: ( IC s = 0 implies for a being Int-Location
for k being Integer st Load (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 )
assume A1: IC s = 0 ; :: thesis: for a being Int-Location
for k being Integer st Load (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 Load (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: ( Load (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: Load (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 + 1) )
assume c < len (aSeq a,k) ; :: thesis: s . (0 + c) = (aSeq a,k) . (c + 1)
then A4: c in dom (Load (aSeq a,k)) by SCMFSA_7:29;
then A5: c + 1 in dom (aSeq a,k) by SCMFSA_7:26;
s . c = (Load (aSeq a,k)) . c by A2, A4, GRFUNC_1:8
.= (aSeq a,k) /. (c + 1) by A4, SCMFSA_7:def 1 ;
hence s . (0 + c) = (aSeq a,k) . (c + 1) by A5, PARTFUN1:def 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 A1, A3, Lm5;
hence IC (Comput (ProgramPart s),s,i) = i ; :: thesis: verum