let I be parahalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for s being State of SCM+FSA holds
( ( f . ((StepWhile=0 a,I,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 Object-Kind of SCM+FSA ),NAT st
for s being State of SCM+FSA holds
( ( f . ((StepWhile=0 a,I,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 Object-Kind of SCM+FSA ),NAT such that A1: for s being State of SCM+FSA holds
( ( f . ((StepWhile=0 a,I,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

let t be State of SCM+FSA ; :: thesis: while=0 a,I is_halting_on t

now

let k be Nat; :: thesis: ( ( f . ((StepWhile=0 a,I,t) . (k + 1)) < f . ((StepWhile=0 a,I,t) . k) or f . ((StepWhile=0 a,I,t) . k) = 0 ) & ( f . ((StepWhile=0 a,I,t) . k) = 0 implies ((StepWhile=0 a,I,t) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,t) . k) . a <> 0 implies f . ((StepWhile=0 a,I,t) . k) = 0 ) )
A2: k in NAT by ORDINAL1:def 13;
( f . ((StepWhile=0 a,I,((StepWhile=0 a,I,t) . k)) . 1) < f . ((StepWhile=0 a,I,t) . k) or f . ((StepWhile=0 a,I,t) . k) = 0 ) by A1;
hence ( ( f . ((StepWhile=0 a,I,t) . (k + 1)) < f . ((StepWhile=0 a,I,t) . k) or f . ((StepWhile=0 a,I,t) . k) = 0 ) & ( f . ((StepWhile=0 a,I,t) . k) = 0 implies ((StepWhile=0 a,I,t) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,t) . k) . a <> 0 implies f . ((StepWhile=0 a,I,t) . k) = 0 ) ) by A1, A2, Th25; :: thesis: verum

end;

hence while=0 a,I is_halting_on t by Th33; :: thesis: verum

end;

hence while=0 a,I is parahalting by SCMFSA7B:25; :: thesis: verum