Skip to content

solve_ndisj: try harder

Ralf Jung requested to merge ralf/solve_ndisj into master

In my logically atomic stack, the following goal fails to be solved currently but is solved after this patch:

⊤ ∖ ↑stackN ⊆ ⊤ ∖ ↑offerN ∖ ↑protoN

where

Definition stackN : namespace := nroot .@ "logatom_stack".
Definition offerN : namespace := nroot .@ "logatom_stack" .@ "offer".
Definition protoN : namespace := nroot .@ "logatom_stack" .@ "protocol".
Edited by Ralf Jung

Merge request reports