let s be 0 -started State of SCMPDS; :: thesis: for n being Element of NAT holds
( (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting )
let n be Element of NAT ; :: thesis: ( (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting )
thus ( (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) ) by Lm8; :: thesis: Fib-macro n is parahalting
for t being State of SCMPDS holds Fib-macro n is_halting_on t

proof

let t be State of SCMPDS; :: thesis: Fib-macro n is_halting_on t
Fib-macro n is_halting_on Initialize t by Lm8;
hence Fib-macro n is_halting_on t by SCMPDS_6:140; :: thesis: verum

end;

hence Fib-macro n is parahalting by SCMPDS_6:35; :: thesis: verum