:: deftheorem defines Fibonacci_main_part NOMIN_7:def 12 :
for V, A being set
for loc being b₁ -valued Function
for val being Function holds Fibonacci_main_part (A,loc,val) = PP_composition ((initial_assignments (A,loc,val,6)),(Fibonacci_main_loop (A,loc)));