let P be Instruction-Sequence of SCMPDS; :: thesis: 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 )
let s be 0 -started State of SCMPDS; :: thesis: 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 )
let n be Element of NAT ; :: thesis: ( (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 )
thus ( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) ) by Lm6; :: thesis: Fib-macro n is parahalting
for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS holds Fib-macro n is_halting_on t,Q
proof
let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS holds Fib-macro n is_halting_on t,Q
let Q be Instruction-Sequence of SCMPDS; :: thesis: Fib-macro n is_halting_on t,Q
Fib-macro n is_halting_on Initialize t,Q by Lm6;
hence Fib-macro n is_halting_on t,Q by SCMPDS_6:126; :: thesis: verum
end;
hence Fib-macro n is parahalting by SCMPDS_6:21; :: thesis: verum