RAIRLab/Peirce-My-Heart

Double Cut can have different Atoms on both layers!

Closed this issue · 0 comments

Describe the bug
When introducing one double cut in Proof Mode, one atom can be in the innermost cut and one atom can be between the innermost and outermost cut.

To Reproduce
Copy atoms A and B from Draw Mode.

Paste them in Proof Mode.

Introduce one double cut such that A is inside both cuts, but B is inside only the outermost cut.

Expected behavior
Double cut introduction should only work for atoms on the innermost cut. Otherwise we can do things like "prove" that truth is false.

Screenshots Or Video
Proof files showcasing the issue will be attached.
[A B]→[(B (A))].json
[A A A A A]→[A A A (A (A))].json
[]→[((()) ())].json