NotExists

class proveit.logic.NotExists(instance_param_or_params, instance_expr, *, domain=None, domains=None, condition=None, conditions=None, styles=None, _lambda_map=None)

Bases: proveit.OperationOverInstances

Methods Summary

conclude_as_folded(self, \*\*defaults_config)	Prove and return some NotExists_{x | Q(x)} P(x) from Not(Exists_{x | Q(x)} P(x)).
side_effects(self, judgment)	Side-effect derivations to attempt automatically for a NotExists operation.
unfold(self, \*\*defaults_config)	Derive and return Not(Exists_{x | Q(x)} P(x)) from NotExists_{x | Q(x)} P(x).

Methods Documentation

conclude_as_folded(self, \*\*defaults_config)

Prove and return some NotExists_{x | Q(x)} P(x) from Not(Exists_{x | Q(x)} P(x)).

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

side_effects(self, judgment)

Side-effect derivations to attempt automatically for a NotExists operation.

unfold(self, \*\*defaults_config)

Derive and return Not(Exists_{x | Q(x)} P(x)) from NotExists_{x | Q(x)} P(x).

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