automatic return set inference: now 'compose(S_1, S_2, S_3, g, h) $in fn(S_1) S_3' is necessary, in the future it should be automated.

[malloc-realloc]

fn compose(set1, set2, set3 nonempty_set, f fn(set2) set3, g fn(set1) set2) fn(set1) set3:
forall x set1:
compose(set1, set2, set3, f, g)(x) = f(g(x))

claim:
@function_composition_associativity(S_1, S_2, S_3, S_4 nonempty_set, f fn(S_3) S_4, g fn(S_2) S_3, h fn(S_1) S_2, x S_1):
compose(S_1, S_3, S_4, f, compose(S_1, S_2, S_3, g, h))(x) = compose(S_1, S_2, S_4, compose(S_2, S_3, S_4, f, g), h)(x) prove: compose(S_1, S_2, S_3, g, h) $in fn(S_1) S_3 =: compose(S_1, S_3, S_4, f, compose(S_1, S_2, S_3, g, h))(x) f(compose(S_1, S_2, S_3, g, h)(x)) f(g(h(x))) =: compose(S_1, S_2, S_4, compose(S_2, S_3, S_4, f, g), h)(x) compose(S_2, S_3, S_4, f, g)(h(x)) f(g(h(x)))