let f be FinSeq-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 f in UsedI*Loc I holds

(Comput (P,s,n)) . f = s . f

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 f in UsedI*Loc I holds

(Comput (P,s,n)) . f = s . f

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 f in UsedI*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 Nat st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedI*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 Nat st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedI*Loc I implies (Comput (P,s,n)) . f = s . f )

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 f in UsedI*Loc I ; :: thesis: (Comput (P,s,n)) . f = s . f

defpred S_{1}[ Nat] means ( $1 <= n implies (Comput (P,s,$1)) . f = s . f );

A4: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A11, A4);

hence (Comput (P,s,n)) . f = s . f ; :: thesis: verum

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 f in UsedI*Loc I holds

(Comput (P,s,n)) . f = s . f

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 f in UsedI*Loc I holds

(Comput (P,s,n)) . f = s . f

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 f in UsedI*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 Nat st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedI*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 Nat st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedI*Loc I implies (Comput (P,s,n)) . f = s . f )

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 f in UsedI*Loc I ; :: thesis: (Comput (P,s,n)) . f = s . f

defpred S

A4: for m being Nat st S

S

proof

A11:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

set sm = Comput (P,s,m);

assume A5: ( m <= n implies (Comput (P,s,m)) . f = s . f ) ; :: thesis: S_{1}[m + 1]

assume A6: m + 1 <= n ; :: thesis: (Comput (P,s,(m + 1))) . f = s . f

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 A7, A1, GRFUNC_1:2;

then UsedInt*Loc (P . (IC (Comput (P,s,m)))) c= UsedI*Loc I by A8, Th35;

then A10: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) by A3;

thus (Comput (P,s,(m + 1))) . f = (Following (P,(Comput (P,s,m)))) . f by EXTPRO_1:3

.= s . f by A5, A6, A10, Th62, A9, NAT_1:13 ; :: thesis: verum

end;set sm = Comput (P,s,m);

assume A5: ( m <= n implies (Comput (P,s,m)) . f = s . f ) ; :: thesis: S

assume A6: m + 1 <= n ; :: thesis: (Comput (P,s,(m + 1))) . f = s . f

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 A7, A1, GRFUNC_1:2;

then UsedInt*Loc (P . (IC (Comput (P,s,m)))) c= UsedI*Loc I by A8, Th35;

then A10: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) by A3;

thus (Comput (P,s,(m + 1))) . f = (Following (P,(Comput (P,s,m)))) . f by EXTPRO_1:3

.= s . f by A5, A6, A10, Th62, A9, NAT_1:13 ; :: thesis: verum

for m being Nat holds S

hence (Comput (P,s,n)) . f = s . f ; :: thesis: verum