diff options
Diffstat (limited to 'source/Test/Unit/Symdiff.hs')
| -rw-r--r-- | source/Test/Unit/Symdiff.hs | 132 |
1 files changed, 0 insertions, 132 deletions
diff --git a/source/Test/Unit/Symdiff.hs b/source/Test/Unit/Symdiff.hs deleted file mode 100644 index ec62fda..0000000 --- a/source/Test/Unit/Symdiff.hs +++ /dev/null @@ -1,132 +0,0 @@ -module Test.Unit.Symdiff where - -import Base -import Bound.Scope -import Bound.Var -import Syntax.Internal -import Filter -import Report.Location - -import Data.Map qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text - -mixfix :: [Maybe Token] -> FunctionSymbol -mixfix pat = mkMixfixItem pat (markerFromPattern pat) NonAssoc - where - markerFromPattern = \case - Just tok : _ -> markerFromToken tok - Nothing : rest -> markerFromPattern rest - [] -> Marker "mixfix" - -subsetSymbol :: RelationSymbol -subsetSymbol = - RelationSymbol (Command "subset") zeroParameterArity "subset" - -adjInhabited :: LexicalItem -adjInhabited = mkLexicalItem [Just (Word "inhabited")] "inhabited" - -adjDisjointFrom :: LexicalItem -adjDisjointFrom = mkLexicalItem [Just (Word "disjoint"), Just (Word "from"), Nothing] "disjoint" - -filtersWell :: Bool -filtersWell = badFact `notElem` (hypothesisFormula <$> taskHypotheses (filterTask symdiff)) - - -handlesStructAndApply :: Bool -handlesStructAndApply = - let - structOp = StructSymbol "foo_op" - structTerm = TermSymbolStruct structOp (Just (TermVar (NamedVar "A"))) - formula = Apply (TermVar (NamedVar "f")) (structTerm :| []) - hypo = Hypothesis - { hypothesisMarker = Marker "struct_apply" - , hypothesisFormula = formula - } - in Map.member hypo (relevantFacts passmark formula (Set.singleton hypo)) - - -badFact :: ExprOf a -badFact = Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "FreshReplacementVar")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Quantified Existentially (Scope (Connected Conjunction (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "A"))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "b")), TermVar (F (TermVar (B (NamedVar "B"))))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (F (TermVar (B (NamedVar "FreshReplacementVar")))), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]])))))) - - -symdiff :: Task -symdiff = - Task - { taskDirectness = Direct - , taskLocation = Nowhere - , taskConjectureLabel = Marker "symdiff_test" - , taskHypotheses = zipWith - Hypothesis - (Marker . Text.pack . show <$> ([1..] :: [Int])) - [ Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))], TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "C"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "x"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []], TermVar (B (NamedVar "x"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "symdiff"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "x"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermVar (B (NamedVar "Z"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermVar (B (NamedVar "Z"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))], TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []], TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "C"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))]]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "inters"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "A"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "A"))]], TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]], TermVar (B (NamedVar "a"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]], TermVar (B (NamedVar "b"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "A"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) [], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "A"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation NeqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermVar (B (NamedVar "a"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation NeqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermVar (B (NamedVar "b"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "A"))])) - , Quantified Universally (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) [], TermVar (B (NamedVar "a"))])) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjDisjointFrom)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjDisjointFrom)) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))])))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]]) (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "Y"))])))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation NeqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Existentially (Scope (Connected ExclusiveOr (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "A"))))]) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "B"))))]))) (Connected Conjunction (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "A"))))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "B"))))]))))))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "B"))]))) - , Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "Y"))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]]))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "C"))]))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (PropositionalConstant IsTop) (PropositionalConstant IsTop)) (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Disjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))))) - , Quantified Universally (Scope (Connected Implication (Connected Conjunction (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "x"))])) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "y"))]))) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]))) - , Quantified Universally (Scope (Connected Implication (Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "A"))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "B"))))])))) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjDisjointFrom)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Not Nowhere (Quantified Existentially (Scope (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "B"))))))]))))))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "A"))]) (Quantified Universally (Scope (Quantified Existentially (Scope (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]))))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "A"))]) (Not Nowhere (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "A"))]))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "aprime")), TermVar (B (NamedVar "bprime"))]]) (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "aprime"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "bprime"))])))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "c"))]], TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "aprime")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Word "pair")])) [TermVar (B (NamedVar "bprime")), TermVar (B (NamedVar "cprime"))]]]) (Connected Conjunction (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "aprime"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "bprime"))])) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "c")), TermVar (B (NamedVar "cprime"))])))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "B")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "A"))]]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]))) - , badFact - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))])))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "x")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "X"))]]) (Connected Disjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))])))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "z")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "inters"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "X"))]]) (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "X"))]) (Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "Y")), TermVar (F (TermVar (B (NamedVar "X"))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (F (TermVar (B (NamedVar "z")))), TermVar (B (NamedVar "Y"))]))))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "z")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "X"))]]) (Quantified Existentially (Scope (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "Y")), TermVar (F (TermVar (B (NamedVar "X"))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (F (TermVar (B (NamedVar "z")))), TermVar (B (NamedVar "Y"))])))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation subsetSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Connected Conjunction (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (F (TermVar (B (NamedVar "A")))), TermVar (F (TermVar (B (NamedVar "B"))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation NeqSymbol)) [TermVar (F (TermVar (B (NamedVar "A")))), TermVar (F (TermVar (B (NamedVar "B"))))])))))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation EqSymbol)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "A"))]))) - , Quantified Universally (Scope (Connected Equivalence (TermSymbol Nowhere (SymbolPredicate (PredicateRelation SubseteqSymbol)) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "B"))))))])))))))) - , Quantified Universally (Scope (Connected Equivalence (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "times"), Nothing])) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]])) (Connected Disjunction (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "X"))])) (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateAdj adjInhabited)) [TermVar (B (NamedVar "Y"))]))))) - , Quantified Universally (Scope (Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (F (TermVar (B (NamedVar "y")))), TermVar (B (NamedVar "X"))]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (F (TermVar (B (NamedVar "y")))), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR])) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]]))))) - , Quantified Universally (Scope (Not Nowhere (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (NamedVar "a")), TermSymbol Nowhere (SymbolMixfix (mixfix [Just (Command "emptyset")])) []]))) - ] - , taskConjecture = - Quantified Universally (Scope (Connected Implication (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (FreshVar 0)), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "setminus"), Nothing])) [TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "union"), Nothing])) [TermVar (F (TermVar (NamedVar "x"))), TermVar (F (TermVar (NamedVar "y")))], TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "inter"), Nothing])) [TermVar (F (TermVar (NamedVar "y"))), TermVar (F (TermVar (NamedVar "x")))]]]) (TermSymbol Nowhere (SymbolPredicate (PredicateRelation ElementSymbol)) [TermVar (B (FreshVar 0)), TermSymbol Nowhere (SymbolMixfix (mixfix [Nothing, Just (Command "symdiff"), Nothing])) [TermVar (F (TermVar (NamedVar "x"))), TermVar (F (TermVar (NamedVar "y")))]]))) - } |