let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a
let I be Program of SCM+FSA; :: thesis: for a being Int-Location st not I destroys a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a
let a be Int-Location ; :: thesis: ( not I destroys a implies for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a )
assume A1: not I destroys a ; :: thesis: for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a
set s1 = s +* (I +* (Start-At (0,SCM+FSA)));
let m be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ) implies for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a )
defpred S₁[ Nat] means ( $1 <= m implies (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1)) . a = s . a );
assume A2: for n being Element of NAT st n < m holds
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) in dom I ; :: thesis: for n being Element of NAT st n <= m holds
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: k + 0 < k + 1 by XREAL_1:8;
assume A6: k + 1 <= m ; :: thesis: (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) . a = s . a
then k < m by A5, XXREAL_0:2;
then IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) in dom I by A2;
hence (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) . a = s . a by A1, A4, A6, A5, Th93, XXREAL_0:2; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n <= m implies (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a )
assume A7: n <= m ; :: thesis: (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a
(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) . a = (s +* (I +* (Start-At (0,SCM+FSA)))) . a by EXTPRO_1:3
.= s . a by Th28 ;
then A8: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A3);
hence (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) . a = s . a by A7; :: thesis: verum