:: deftheorem defines initial_assignments NOMIN_7:def 9 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for size being Nat holds initial_assignments (A,loc,val,size) = (initial_assignments_Seq (A,loc,val,size)) . size;