unbundle

proveit.unbundle(expr, unbundle_thm, num_param_entries=(1, ), \*\*defaults_config)

Given a nested OperationOverInstances, derive or equate an equivalent form in which the parameter entries are split in number according to ‘num_param_entries’. Use the given theorem specific to the particular OperationOverInstances.

For example,

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

can become

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

via bundle with num_param_entries=(2, 1) or num_param_entries=(2,) – the last number can be implied by the remaining number of parameters.

For example of the form of the theorem required, see proveit.logic.booleans.quantification.unbundling or proveit.logic.booleans.quantification.bundling_equality.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.