let I be InitHalting good really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) implies while>0 (a,I) is InitHalting )

assume A1: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ; :: thesis: while>0 (a,I) is InitHalting

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) holds

while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) implies while>0 (a,I) is InitHalting )

assume A1: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ; :: thesis: while>0 (a,I) is InitHalting

now :: thesis: for t being State of SCM+FSA

for Q being Instruction-Sequence of SCM+FSA st t . a > 0 holds

(IExec (I,Q,t)) . a < t . a

hence
while>0 (a,I) is InitHalting
by SCM_HALT:76; :: thesis: verumfor Q being Instruction-Sequence of SCM+FSA st t . a > 0 holds

(IExec (I,Q,t)) . a < t . a

let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st t . a > 0 holds

(IExec (I,b_{3},b_{2})) . a < b_{2} . a

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a > 0 implies (IExec (I,b_{2},b_{1})) . a < b_{1} . a )

assume A2: t . a > 0 ; :: thesis: (IExec (I,b_{2},b_{1})) . a < b_{1} . a

end;(IExec (I,b

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a > 0 implies (IExec (I,b

assume A2: t . a > 0 ; :: thesis: (IExec (I,b