let s be State of SCM+FSA ; :: thesis: ( IC s = insloc 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 (Computation s,i) = insloc i )
assume A1: IC s = insloc 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 (Computation s,i) = insloc 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 (Computation s,i) = insloc 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 (Computation s,i) = insloc i )
assume A2: Load (aSeq a,k) c= s ; :: thesis: for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Computation s,i) = insloc i
let i be Element of NAT ; :: thesis: ( i <= len (aSeq a,k) implies IC (Computation s,i) = insloc i )
assume A3: i <= len (aSeq a,k) ; :: thesis: IC (Computation s,i) = insloc i

now

let c be Element of NAT ; :: thesis: ( c < len (aSeq a,k) implies s . (insloc (0 + c)) = (aSeq a,k) . (c + 1) )
assume c < len (aSeq a,k) ; :: thesis: s . (insloc (0 + c)) = (aSeq a,k) . (c + 1)
then A4: insloc 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 . (insloc c) = (Load (aSeq a,k)) . (insloc c) by A2, A4, GRFUNC_1:8
.= (aSeq a,k) /. (c + 1) by A4, SCMFSA_7:def 1 ;
hence s . (insloc (0 + c)) = (aSeq a,k) . (c + 1) by A5, PARTFUN1:def 8; :: thesis: verum

end;

then IC (Computation s,i) = insloc (0 + i) by A1, A3, Lm5;
hence IC (Computation s,i) = insloc i ; :: thesis: verum