:: deftheorem defines Fibonacci_program NOMIN_7:def 13 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for z being Element of V holds Fibonacci_program (A,loc,val,z) = PP_composition ((Fibonacci_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));