:: deftheorem defines Fibonacci_loop_body NOMIN_7:def 10 :
for V, A being set
for loc being b₁ -valued Function holds Fibonacci_loop_body (A,loc) = PP_composition ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))),(SC_assignment ((addition (A,(loc /. 6),(loc /. 4))),(loc /. 5))),(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))));