Skip to content

Conversation

@wdcraft01
Copy link
Collaborator

This branch updates the SubsetEq.conclude() method (in logic/sets/inclusion) to deal more correctly with the special case of "basic" SetOfAll set comprehensions. Some errors had recently been encountered due to some older code in the conclude() method. The use of SetOfAll.explicit_conditions() (instead of the more general .conditions()) and wrapping conditions in a logical And() seems to have corrected the most basic problems. Branch also includes updated related demonstrations notebook in logic/sets/inclusion and minor addition to demonstrations notebook in logic/sets/comprehension.

Update SubsetEq.conclude() method to deal more correctly with the special case of "basic" SetOfAll set comprehensions. Errors has been recently encountered due to some older code in the conclude() method. The use of SetOfAll.explicit_conditions() (instead of the more general .conditions()) and wrapping conditions in a logical And() seems to have corrected the most basic problems. Commit also includes updated related demonstrations ntoebook in logic/sets/inclusion and minor addition to demonstrations notebook in logic/sets/comprehension.
@wdcraft01 wdcraft01 requested a review from wwitzel November 6, 2025 17:11
@wdcraft01 wdcraft01 linked an issue Nov 6, 2025 that may be closed by this pull request
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

SubsetEq(A, B).conclude() proof failure

2 participants