let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )
let s be 0 -started State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies for a being Int-Location
for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) )
assume A1: s . (intloc 0) = 1 ; :: thesis: for a being Int-Location
for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )
let a be Int-Location; :: thesis: for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )
let k be Integer; :: thesis: ( aSeq (a,k) c= P & a <> intloc 0 implies ( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) )
assume that
A2: aSeq (a,k) c= P and
A3: a <> intloc 0 ; :: thesis: ( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )
A4: for c being Nat st c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (0 + c) by A2, GRFUNC_1:2;

hereby :: thesis: (Comput (P,s,(len (aSeq (a,k))))) . a = k

let i be Nat; :: thesis: ( i <= len (aSeq (a,k)) implies ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) )
assume A5: i <= len (aSeq (a,k)) ; :: thesis: ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) )
then IC (Comput (P,s,i)) = 0 + i by A1, A3, A4, Th4;
hence ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) by A1, A3, A4, A5, Th4; :: thesis: verum

end;

thus (Comput (P,s,(len (aSeq (a,k))))) . a = k by A1, A3, A4, Th4; :: thesis: verum