let I be really-closed parahalting MacroInstruction of SCM+FSA ; 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; ( 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 ) )
; while=0 (a,I) is parahalting
now for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA holds while=0 (a,I) is_halting_on t,Qlet t be
State of
SCM+FSA;
for Q being Instruction-Sequence of SCM+FSA holds while=0 (a,I) is_halting_on t,Qlet Q be
Instruction-Sequence of
SCM+FSA;
while=0 (a,I) is_halting_on t,Qnow 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;
( ( 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, Th5;
verum end; hence
while=0 (
a,
I)
is_halting_on t,
Q
by Th9;
verum end;
hence
while=0 (a,I) is parahalting
by SCMFSA7B:19; verum