:: deftheorem defines Fibonacci_main_loop NOMIN_7:def 11 :
for V, A being set
for loc being b₁ -valued Function holds Fibonacci_main_loop (A,loc) = PP_while ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(Fibonacci_loop_body (A,loc)));