theorem :: SCPINVAR:7

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for n being Element of NAT holds
( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is parahalting )