let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )
let s be State of SCM+FSA; :: thesis: for I being really-closed good InitHalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )
let I be really-closed good InitHalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st not I destroys a holds
( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )
let a be read-write Int-Location; :: thesis: ( not I destroys a implies ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) ) )
assume A1: not I destroys a ; :: thesis: ( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )
set I1 = I ";" (SubFrom (a,(intloc 0)));
set ss = IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s);
set s0 = Initialized s;
thus (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 by A1, Lm10; :: thesis: ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) )
assume A2: s . a > 0 ; :: thesis: DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s))))
reconsider II = I ";" (SubFrom (a,(intloc 0))) as really-closed good InitHalting MacroInstruction of SCM+FSA ;
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds
(IExec (II,P,s)) . a < s . a

proof

let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds
(IExec (II,P,s)) . a < s . a
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( s . a > 0 implies (IExec (II,P,s)) . a < s . a )
assume s . a > 0 ; :: thesis: (IExec (II,P,s)) . a < s . a
(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 by A1, Lm10;
hence (IExec (II,P,s)) . a < s . a by XREAL_1:44; :: thesis: verum

end;

then Times (a,I) is InitHalting by Lm9;
then DataPart (IExec ((while>0 (a,II)),p,s)) = DataPart (IExec ((while>0 (a,II)),p,(IExec (II,p,s)))) by A2, Lm8;
hence DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ; :: thesis: verum