let I be really-closed parahalting MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . ((StepWhile>0 (a,I,P,s)) . 1) < f . s or f . s = 0 ) & ( f . s = 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s = 0 ) ) holds
while>0 (a,I) is parahalting
let a be read-write Int-Location; :: thesis: ( ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . ((StepWhile>0 (a,I,P,s)) . 1) < f . s or f . s = 0 ) & ( f . s = 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s = 0 ) ) implies while>0 (a,I) is parahalting )
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A1: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . ((StepWhile>0 (a,I,P,s)) . 1) < f . s or f . s = 0 ) & ( f . s = 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s = 0 ) ) ; :: thesis: while>0 (a,I) is parahalting

now :: thesis: for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_on t,Q

let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_on t,Q
let Q be Instruction-Sequence of SCM+FSA; :: thesis: while>0 (a,I) is_halting_on t,Q

now :: thesis: for k being Nat holds
( ( f . ((StepWhile>0 (a,I,Q,t)) . (k + 1)) < f . ((StepWhile>0 (a,I,Q,t)) . k) or f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) & ( f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 implies ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) )

let k be Nat; :: thesis: ( ( f . ((StepWhile>0 (a,I,Q,t)) . (k + 1)) < f . ((StepWhile>0 (a,I,Q,t)) . k) or f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) & ( f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 implies ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) )
( f . ((StepWhile>0 (a,I,Q,((StepWhile>0 (a,I,Q,t)) . k))) . 1) < f . ((StepWhile>0 (a,I,Q,t)) . k) or f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) by A1;
hence ( ( f . ((StepWhile>0 (a,I,Q,t)) . (k + 1)) < f . ((StepWhile>0 (a,I,Q,t)) . k) or f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) & ( f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 implies ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,I,Q,t)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,Q,t)) . k) = 0 ) ) by A1, Th16; :: thesis: verum

end;

hence while>0 (a,I) is_halting_on t,Q by Th20; :: thesis: verum

end;

hence while>0 (a,I) is parahalting by SCMFSA7B:19; :: thesis: verum