let f be FinSeq-Location ; :: thesis: for I being Program of
for n being Element of NAT
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput (P,s,n)) . f = s . f
let I be Program of ; :: thesis: for n being Element of NAT
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput (P,s,n)) . f = s . f
let n be Element of NAT ; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput (P,s,n)) . f = s . f
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds
(Comput (P,s,n)) . f = s . f
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= P & ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I implies (Comput (P,s,n)) . f = s . f )
assume that
A2: I c= P and
A3: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I and
A4: not f in UsedInt*Loc I ; :: thesis: (Comput (P,s,n)) . f = s . f
defpred S₁[ Nat] means ( $1 <= n implies (Comput (P,s,$1)) . f = s . f );
A5: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
set sm = Comput (P,s,m);
assume A6: ( m <= n implies (Comput (P,s,m)) . f = s . f ) ; :: thesis: S₁[m + 1]
assume A7: m + 1 <= n ; :: thesis: (Comput (P,s,(m + 1))) . f = s . f
then m < n by NAT_1:13;
then A8: IC (Comput (P,s,m)) in dom I by A3;
then A9: I . (IC (Comput (P,s,m))) in rng I by FUNCT_1:def 3;
dom P = NAT by PARTFUN1:def 2;
then A10: 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 A8, A2, GRFUNC_1:2;
then UsedInt*Loc (P . (IC (Comput (P,s,m)))) c= UsedInt*Loc I by A9, Th39;
then A11: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) by A4;
thus (Comput (P,s,(m + 1))) . f = (Following (P,(Comput (P,s,m)))) . f by EXTPRO_1:3
.= s . f by A6, A7, A11, Th70, A10, NAT_1:13 ; :: thesis: verum

end;

A12: S₁[ 0 ] by EXTPRO_1:2;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A12, A5);
hence (Comput (P,s,n)) . f = s . f ; :: thesis: verum