let s be 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 by Lm8;
hence Fib-macro n is parahalting by SCMPDS_6:35; :: thesis: verum