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

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

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

then
Times (a,I) is InitHalting
by Lm9;
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;(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

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