let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being really-closed good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1

let s be State of SCM+FSA; :: thesis: for I being really-closed good InitHalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1

let I be really-closed good InitHalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a holds
(IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1

let a be read-write Int-Location; :: thesis: ( not I destroys a implies (IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1 )
assume A1: not I destroys a ; :: thesis: (IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (s . a) - 1
set I1 = I ";" (SubFrom (a,()));
set ss = IExec ((I ";" (SubFrom (a,()))),p,s);
set s0 = Initialized s;
thus (IExec ((I ";" (SubFrom (a,()))),p,s)) . a = (Exec ((SubFrom (a,())),(IExec (I,p,s)))) . a by Th21
.= ((IExec (I,p,s)) . a) - ((IExec (I,p,s)) . ()) by SCMFSA_2:65
.= ((IExec (I,p,s)) . a) - 1 by Th7
.= (() . a) - 1 by
.= (s . a) - 1 by SCMFSA_M:37 ; :: thesis: verum