let I be parahalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )
let s be State of SCM+FSA ; :: thesis: ( ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) implies ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s ) )
A1: ( ( for k being Nat holds I is_closed_on (StepWhile=0 a,I,s) . k ) & ( for k being Nat holds I is_halting_on (StepWhile=0 a,I,s) . k ) ) by SCMFSA7B:24, SCMFSA7B:25;
assume ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) ; :: thesis: ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )
hence ( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s ) by A1, Th32; :: thesis: verum