On the Compositions of Macro Instructions. Part I
Andrzej Trybulec, Yatsuka Nakamura, Noriko Asamoto · 1997
One can prove the following propositions: (1) For all functions f , g and for all sets x, y such that g ⊆ f and x / ∈ dom g holds g ⊆ f +· (x, y). (2) For all functions f , g and for every set A such that f A = g A and f and g are equal outside A holds f = g. (3) For every function f and for all sets a, b, A such that a ∈ A holds f and f +· (a, b) are equal outside A. (4) For every function f and for all sets a, b, A holds a ∈ A or (f +· (a, b)) A = f A. (5) For all functions f , g and for all sets a, b, A such that f A = g A holds (f +· (a, b)) A = (g +· (a, b)) A. (6) For all functions f , g, h such that f ⊆ h and g ⊆ h holds f+·g ⊆ h. (7) For arbitrary a, b and for every function f holds a7−→ . b ⊆ f iff a ∈ dom f and f(a) = b. (8) For every function f and for every set A holds dom(f (dom f A)) = dom f A.