let a be Int-Location ; :: thesis: for I being Program of SCM+FSA
for n being Element of NAT
for s being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s & ( for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I ) & not a in UsedIntLoc I holds
(Computation s,n) . a = s . a
let I be Program of SCM+FSA ; :: thesis: for n being Element of NAT
for s being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s & ( for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I ) & not a in UsedIntLoc I holds
(Computation s,n) . a = s . a
let n be Element of NAT ; :: thesis: for s being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s & ( for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I ) & not a in UsedIntLoc I holds
(Computation s,n) . a = s . a
let s be State of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s & ( for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I ) & not a in UsedIntLoc I implies (Computation s,n) . a = s . a )
assume A1: ( I +* (Start-At (insloc 0 )) c= s & ( for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I ) & not a in UsedIntLoc I ) ; :: thesis: (Computation s,n) . a = s . a
defpred S₁[ Element of NAT ] means ( $1 <= n implies (Computation s,$1) . a = s . a );
A2: S₁[ 0 ] by AMI_1:13;
A3: 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 = Computation s,m;
assume A4: ( m <= n implies (Computation s,m) . a = s . a ) ; :: thesis: S₁[m + 1]
assume A5: m + 1 <= n ; :: thesis: (Computation s,(m + 1)) . a = s . a
then m < n by NAT_1:13;
then A6: IC (Computation s,m) in dom I by A1;
then A7: I . (IC (Computation s,m)) in rng I by FUNCT_1:def 5;
dom I misses dom (Start-At (insloc 0 )) by Th64;
then I c= I +* (Start-At (insloc 0 )) by FUNCT_4:33;
then I c= s by A1, XBOOLE_1:1;
then I c= Computation s,m by AMI_1:81;
then I . (IC (Computation s,m)) = (Computation s,m) . (IC (Computation s,m)) by A6, GRFUNC_1:8;
then UsedIntLoc ((Computation s,m) . (IC (Computation s,m))) c= UsedIntLoc I by A7, Th23;
then A8: not a in UsedIntLoc ((Computation s,m) . (IC (Computation s,m))) by A1;
thus (Computation s,(m + 1)) . a = (Following (Computation s,m)) . a by AMI_1:14
.= s . a by A4, A5, A8, Th68, NAT_1:13 ; :: thesis: verum

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
hence (Computation s,n) . a = s . a ; :: thesis: verum