let a be Int-Location; :: thesis: for I being Program of
for n being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc I holds
(Comput (P,s,n)) . a = s . a

let I be Program of ; :: thesis: for n being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc I holds
(Comput (P,s,n)) . a = s . a

let n be Nat; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc I holds
(Comput (P,s,n)) . a = s . a

let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc I holds
(Comput (P,s,n)) . a = s . a

let P be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc I implies (Comput (P,s,n)) . a = s . a )

assume that
A1: I c= P and
A2: for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I and
A3: not a in UsedILoc I ; :: thesis: (Comput (P,s,n)) . a = s . a
defpred S1[ Nat] means ( \$1 <= n implies (Comput (P,s,\$1)) . a = s . a );
A4: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
set sm = Comput (P,s,m);
assume A5: ( m <= n implies (Comput (P,s,m)) . a = s . a ) ; :: thesis: S1[m + 1]
assume A6: m + 1 <= n ; :: thesis: (Comput (P,s,(m + 1))) . a = s . a
then m < n by NAT_1:13;
then A7: IC (Comput (P,s,m)) in dom I by A2;
then A8: I . (IC (Comput (P,s,m))) in rng I by FUNCT_1:def 3;
dom P = NAT by PARTFUN1:def 2;
then A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def 6;
I . (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by ;
then UsedIntLoc (P . (IC (Comput (P,s,m)))) c= UsedILoc I by ;
then A10: not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) by A3;
thus (Comput (P,s,(m + 1))) . a = (Following (P,(Comput (P,s,m)))) . a by EXTPRO_1:3
.= s . a by ; :: thesis: verum
end;
A11: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A11, A4);
hence (Comput (P,s,n)) . a = s . a ; :: thesis: verum