Compare commits
6 changed files with 205 additions and 314 deletions
74
Main.hs
74
Main.hs
|
|
@ -1,73 +1,27 @@
|
||||||
module Main (main) where
|
module Main (main) where
|
||||||
|
import Prelude (IO, String, getContents, lines, map, print,
|
||||||
import Data.Foldable (Foldable, any)
|
otherwise, Bool(..), filter, id, unlines,
|
||||||
import Data.List (head, tail)
|
mapM_, ($), elem, notElem, (||), putStrLn, read, (.))
|
||||||
import Data.Maybe (isNothing)
|
|
||||||
import GHC.Base (Maybe (..), (==))
|
|
||||||
import System.Environment (getArgs)
|
|
||||||
import Ternary.Statement (Statement (..), st)
|
import Ternary.Statement (Statement (..), st)
|
||||||
import Ternary.Term (Item (..), Term (..))
|
|
||||||
import Ternary.Universum (Universum (..), universum)
|
import Ternary.Universum (Universum (..), universum)
|
||||||
import Ternary.Vee (cleared, hasContradiction, think)
|
import Ternary.Vee (cleared, think)
|
||||||
import Prelude
|
import System.Environment (getArgs)
|
||||||
( Bool (..),
|
import Data.Foldable (Foldable)
|
||||||
IO,
|
|
||||||
String,
|
|
||||||
elem,
|
|
||||||
filter,
|
|
||||||
getContents,
|
|
||||||
id,
|
|
||||||
lines,
|
|
||||||
map,
|
|
||||||
mapM_,
|
|
||||||
notElem,
|
|
||||||
otherwise,
|
|
||||||
print,
|
|
||||||
putStrLn,
|
|
||||||
read,
|
|
||||||
unlines,
|
|
||||||
($),
|
|
||||||
(.),
|
|
||||||
(||),
|
|
||||||
)
|
|
||||||
|
|
||||||
mainSolve :: Universum -> Bool -> IO ()
|
main2 :: Universum -> Bool -> IO ()
|
||||||
mainSolve u onlyNew = do
|
main2 u onlyNew = do
|
||||||
strs <- getContents
|
strs <- getContents
|
||||||
let statements = map str2vee . lines $ strs
|
let statements = map str2vee . lines $ strs
|
||||||
str2vee x = st (read x :: Statement String)
|
str2vee x = st (read x :: Statement String)
|
||||||
mapM_ print
|
mapM_ print
|
||||||
. (if onlyNew then filter (`notElem` statements) else id)
|
. (if onlyNew then filter (`notElem` statements) else id)
|
||||||
. cleared
|
. cleared
|
||||||
. think (universum u)
|
. think (universum u) $ statements
|
||||||
$ statements
|
|
||||||
|
|
||||||
mainProve :: Universum -> Bool -> IO ()
|
|
||||||
mainProve u onlyNew = do
|
|
||||||
strs <- getContents
|
|
||||||
let statements = map str2vee . tail . lines $ strs
|
|
||||||
proveThis = str2vee . head . lines $ strs
|
|
||||||
str2vee x = st (read x :: Statement String)
|
|
||||||
results = cleared . think (universum u) $ statements
|
|
||||||
anyContradictions = any (hasContradiction proveThis) results
|
|
||||||
proof = swapNothingJF $ if anyContradictions then Nothing else Just (Item recalc == Item results)
|
|
||||||
recalc = cleared . think (universum u) $ proveThis : statements
|
|
||||||
swapNothingJF x
|
|
||||||
| isNothing x = Just False
|
|
||||||
| x == Just False = Nothing
|
|
||||||
| x == Just True = Just True
|
|
||||||
|
|
||||||
print recalc
|
|
||||||
putStrLn ""
|
|
||||||
print results
|
|
||||||
putStrLn ""
|
|
||||||
print proof
|
|
||||||
|
|
||||||
withArgs :: (String -> Bool) -> IO ()
|
withArgs :: (String -> Bool) -> IO ()
|
||||||
withArgs a
|
withArgs a
|
||||||
| a "-h" || a "--help" =
|
| a "-h" || a "--help" = putStrLn . unlines $
|
||||||
putStrLn . unlines $
|
["Logical statement solver",
|
||||||
[ "Logical statement solver",
|
|
||||||
"Usage: solver [PARAMETERS]",
|
"Usage: solver [PARAMETERS]",
|
||||||
"",
|
"",
|
||||||
"Designed according to N.P.Brousentsov works",
|
"Designed according to N.P.Brousentsov works",
|
||||||
|
|
@ -82,13 +36,11 @@ withArgs a
|
||||||
"",
|
"",
|
||||||
"A \"Socrates\" \"human\"",
|
"A \"Socrates\" \"human\"",
|
||||||
"",
|
"",
|
||||||
"There are A, E, O, I traditional statements.",
|
"There are A, E, O, I traditional statements exist.",
|
||||||
"Also there are A~, E~, O~, I~ with negated first part"
|
"Also there are A~, E~, O~, I~ with negated first part"
|
||||||
]
|
]
|
||||||
| a "--version" || a "-v" = putStrLn "v1.0.2"
|
| a "--version" || a "-v" = putStrLn "v1.0.2"
|
||||||
| a "--prove" = mainProve Aristotle False
|
| otherwise = main2 uni onlyNew where
|
||||||
| otherwise = mainSolve uni onlyNew
|
|
||||||
where
|
|
||||||
onlyNew = a "--new" || a "-n"
|
onlyNew = a "--new" || a "-n"
|
||||||
uni =
|
uni =
|
||||||
if a "-A" || a "--aristotle"
|
if a "-A" || a "--aristotle"
|
||||||
|
|
|
||||||
|
|
@ -6,7 +6,7 @@
|
||||||
|
|
||||||
Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве.
|
Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве.
|
||||||
|
|
||||||
Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсутствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях.
|
Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсуствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях.
|
||||||
|
|
||||||
Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно.
|
Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,18 +1,14 @@
|
||||||
module Ternary.Statement (Statement(..), st) where
|
module Ternary.Statement (Statement(..), st) where
|
||||||
import Ternary.Term (Vee, Term(..), Item(..))
|
import Ternary.Term (Vee, Term(..), Item(..))
|
||||||
|
data Statement a = A a a -- Affirmo (general affirmative)
|
||||||
data StatementKind = A | I | E | O | A' | I' | E' | O' deriving (Eq, Show, Read)
|
| I a a -- affIrmo (private affirmative)
|
||||||
data Statement a = Statement StatementKind a a deriving (Eq, Read)
|
| E a a -- nEgo (general negative)
|
||||||
|
| O a a -- negO (private negative)
|
||||||
instance Show a => Show (Statement a) where
|
| A' a a
|
||||||
show (Statement A x y) = "Every " ++ show x ++ " is " ++ show y
|
| I' a a
|
||||||
show (Statement I x y) = "Some of " ++ show x ++ " is " ++ show y
|
| E' a a
|
||||||
show (Statement E x y) = "None of " ++ show x ++ " is " ++ show y
|
| O' a a
|
||||||
show (Statement O x y) = "Some of " ++ show x ++ " isn't " ++ show y
|
deriving (Eq, Show, Read)
|
||||||
show (Statement A' x y) = "Every non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement I' x y) = "Some of non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement E' x y) = "None of non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement O' x y) = "Some of non-" ++ show x ++ " isn't " ++ show y
|
|
||||||
|
|
||||||
inv :: (Eq a) => Term a -> Term a
|
inv :: (Eq a) => Term a -> Term a
|
||||||
inv (Term p x) = Term (not p) x
|
inv (Term p x) = Term (not p) x
|
||||||
|
|
@ -24,11 +20,11 @@ i v x y
|
||||||
| x == y = Term v . Item $ [x]
|
| x == y = Term v . Item $ [x]
|
||||||
|
|
||||||
st :: (Eq a) => Statement a -> Vee a
|
st :: (Eq a) => Statement a -> Vee a
|
||||||
st (Statement A x y) = i False (Term True x) (Term False y)
|
st (A x y) = i False (Term True x) (Term False y)
|
||||||
st (Statement I x y) = i True (Term True x) (Term True y)
|
st (I x y) = i True (Term True x) (Term True y)
|
||||||
st (Statement E x y) = i False (Term True x) (Term True y)
|
st (E x y) = i False (Term True x) (Term True y)
|
||||||
st (Statement O x y) = i True (Term True x) (Term False y)
|
st (O x y) = i True (Term True x) (Term False y)
|
||||||
st (Statement A' x y) = i False (Term False x) (Term False y)
|
st (A' x y) = i False (Term False x) (Term False y)
|
||||||
st (Statement I' x y) = i True (Term False x) (Term True y)
|
st (I' x y) = i True (Term False x) (Term True y)
|
||||||
st (Statement E' x y) = i False (Term False x) (Term True y)
|
st (E' x y) = i False (Term False x) (Term True y)
|
||||||
st (Statement O' x y) = i True (Term False x) (Term False y)
|
st (O' x y) = i True (Term False x) (Term False y)
|
||||||
|
|
|
||||||
140
Ternary/Vee.hs
140
Ternary/Vee.hs
|
|
@ -1,48 +1,10 @@
|
||||||
module Ternary.Vee (isObvious, hasContradiction, newFact, cleared, think) where
|
module Ternary.Vee (isObvious, newFact, cleared, think) where
|
||||||
|
import Data.List (head, intersect, length, nub, null, union, (\\))
|
||||||
import Data.Foldable (concatMap)
|
|
||||||
import Data.List
|
|
||||||
( elem,
|
|
||||||
filter,
|
|
||||||
head,
|
|
||||||
intersect,
|
|
||||||
iterate,
|
|
||||||
length,
|
|
||||||
nub,
|
|
||||||
null,
|
|
||||||
union,
|
|
||||||
(\\),
|
|
||||||
)
|
|
||||||
import Data.Maybe (Maybe (Nothing), mapMaybe)
|
import Data.Maybe (Maybe (Nothing), mapMaybe)
|
||||||
import GHC.Base ((<), (>))
|
import Prelude (Bool (False, True), Eq, any, foldr, fst, map,
|
||||||
import GHC.Maybe (Maybe (..))
|
not, notElem, otherwise, return, snd, ($), (&&),
|
||||||
|
(.), (/=), (<$>), (<*>), (=<<), (==))
|
||||||
import Ternary.Term (Item (..), Term (..), Vee)
|
import Ternary.Term (Item (..), Term (..), Vee)
|
||||||
import Prelude
|
|
||||||
( Bool (False, True),
|
|
||||||
Eq,
|
|
||||||
any,
|
|
||||||
foldr,
|
|
||||||
fst,
|
|
||||||
map,
|
|
||||||
not,
|
|
||||||
notElem,
|
|
||||||
otherwise,
|
|
||||||
return,
|
|
||||||
snd,
|
|
||||||
($),
|
|
||||||
(&&),
|
|
||||||
(.),
|
|
||||||
(/=),
|
|
||||||
(<$>),
|
|
||||||
(<*>),
|
|
||||||
(=<<),
|
|
||||||
(==),
|
|
||||||
)
|
|
||||||
|
|
||||||
type Knowledge a = [Vee a]
|
|
||||||
|
|
||||||
type InferenceRule a = Vee a -> Vee a -> (Knowledge a, Maybe (Vee a))
|
|
||||||
|
|
||||||
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
|
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
|
||||||
a `isSubsetOf` b = nda && not ndb
|
a `isSubsetOf` b = nda && not ndb
|
||||||
where
|
where
|
||||||
|
|
@ -55,64 +17,52 @@ isObvious (Term x (Item a)) (Term y (Item b))
|
||||||
| x = a `isSubsetOf` b
|
| x = a `isSubsetOf` b
|
||||||
| not x = b `isSubsetOf` a
|
| not x = b `isSubsetOf` a
|
||||||
|
|
||||||
hasContradiction :: (Eq a) => Vee a -> Vee a -> Bool
|
newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
|
||||||
hasContradiction (Term x (Item a)) (Term y (Item b))
|
|
||||||
| a == b && x /= y = True
|
|
||||||
| a `isSubsetOf` b && x < y = True
|
|
||||||
| b `isSubsetOf` a && x > y = True
|
|
||||||
| otherwise = False
|
|
||||||
|
|
||||||
notT :: Term a -> Term a
|
|
||||||
notT (Term x v) = Term (not x) v
|
|
||||||
|
|
||||||
rulePosFromNeg :: (Eq a) => InferenceRule a
|
|
||||||
rulePosFromNeg (Term False (Item negSet)) positive@(Term True (Item posSet))
|
|
||||||
| length diff /= 1 = ([], Nothing)
|
|
||||||
| missing `elem` posSet = ([], Nothing)
|
|
||||||
| otherwise = ([positive], Just (Term True (Item (missing : posSet))))
|
|
||||||
where
|
|
||||||
diff = negSet \\ posSet
|
|
||||||
missing = notT (head diff)
|
|
||||||
|
|
||||||
ruleNegFromNeg :: (Eq a) => InferenceRule a
|
|
||||||
ruleNegFromNeg (Term False (Item i0)) (Term False (Item i1))
|
|
||||||
| length evidence /= 1 = ([], Nothing)
|
|
||||||
| null diff0 && null diff1 = (map (Term False . Item) [i0, i1], Just (Term False (Item result)))
|
|
||||||
| otherwise = ([], Just (Term False (Item result)))
|
|
||||||
where
|
|
||||||
evidence = map notT i0 `intersect` i1
|
|
||||||
diff0 = (i0 \\ i1) \\ map notT evidence
|
|
||||||
diff1 = (i1 \\ i0) \\ evidence
|
|
||||||
result = (i0 `intersect` i1) `union` diff0 `union` diff1
|
|
||||||
|
|
||||||
newFact :: (Eq a) => InferenceRule a
|
|
||||||
newFact a@(Term True _) b@(Term False _) = newFact b a
|
newFact a@(Term True _) b@(Term False _) = newFact b a
|
||||||
newFact a@(Term False _) b@(Term True _) = rulePosFromNeg a b
|
newFact (Term False (Item iF)) tT@(Term True (Item iT))
|
||||||
newFact a@(Term False _) b@(Term False _) = ruleNegFromNeg a b
|
| length ldF /= 1 = ([], Nothing)
|
||||||
|
| otherwise =
|
||||||
|
if d'F `notElem` iT
|
||||||
|
then (return tT, return (Term True (Item (d'F:iT))))
|
||||||
|
else ([], Nothing)
|
||||||
|
where
|
||||||
|
ldF = iF \\ iT
|
||||||
|
d'F = notT . head $ ldF
|
||||||
|
notT (Term x v) = Term (not x) v
|
||||||
|
newFact (Term False (Item i0)) (Term False (Item i1))
|
||||||
|
| length e /= 1 = ([], Nothing)
|
||||||
|
| otherwise =
|
||||||
|
if null d0 && null d1
|
||||||
|
then (map (Term False . Item) [i0, i1], vee0)
|
||||||
|
else ([], vee0)
|
||||||
|
where
|
||||||
|
notT (Term x v) = Term (not x) v
|
||||||
|
terms = (i0 `intersect` i1) `union` d0 `union` d1
|
||||||
|
e = map notT i0 `intersect` i1
|
||||||
|
d0 = (i0 \\ i1) \\ map notT e
|
||||||
|
d1 = (i1 \\ i0) \\ e
|
||||||
|
vee0 = return (Term False (Item terms))
|
||||||
newFact _ _ = ([], Nothing)
|
newFact _ _ = ([], Nothing)
|
||||||
|
|
||||||
next :: (Eq a) => (Knowledge a, Knowledge a) -> (Knowledge a, Knowledge a)
|
pseudofix :: (Eq a) => (a -> a) -> a -> a
|
||||||
next (old, new) = (old `union` new \\ used, added)
|
pseudofix f x0
|
||||||
|
| y == y' = y
|
||||||
|
| otherwise = y'
|
||||||
where
|
where
|
||||||
results = [newFact o n | o <- old, n <- new]
|
y = f x0
|
||||||
used = concatMap fst results
|
y' = f y
|
||||||
added = mapMaybe snd results
|
|
||||||
|
|
||||||
applyFacts :: (Eq a) => Knowledge a -> Knowledge a -> Knowledge a
|
next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a])
|
||||||
applyFacts old new =
|
next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r)
|
||||||
fst . head . dropStable $ iterate next (old, new)
|
|
||||||
where
|
where
|
||||||
dropStable (x : y : xs)
|
r = newFact <$> o <*> n
|
||||||
| x == y = [x]
|
|
||||||
| otherwise = dropStable (y : xs)
|
|
||||||
dropStable _ = []
|
|
||||||
|
|
||||||
cleared :: (Eq a) => Knowledge a -> Knowledge a
|
applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
|
||||||
cleared vees = nub $ filter (not . isRedundant) vees
|
applyFacts old new = fst $ pseudofix next (old, new)
|
||||||
where
|
|
||||||
isRedundant v = any (isObvious v) vees
|
|
||||||
|
|
||||||
think :: (Eq a) => (Knowledge a -> Knowledge a) -> Knowledge a -> Knowledge a
|
cleared :: (Eq a) => [Vee a] -> [Vee a]
|
||||||
think addition = foldr (applyFacts . withUni . return) []
|
cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees]
|
||||||
where
|
|
||||||
|
think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a]
|
||||||
|
think addition = foldr (applyFacts . withUni . return) [] where
|
||||||
withUni vees = applyFacts (addition vees) vees
|
withUni vees = applyFacts (addition vees) vees
|
||||||
|
|
|
||||||
192
Tests/syllotest
192
Tests/syllotest
|
|
@ -1,96 +1,96 @@
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement A "x" "z")
|
(A "y" "z", A "x" "y", A "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement E' "x" "z")
|
(A "y" "z", E' "x" "y", E' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement E "x" "z")
|
(E "y" "z", A "x" "y", E "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement A' "x" "z")
|
(E "y" "z", E' "x" "y", A' "x" "z")
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement I "x" "z")
|
(A "y" "z", A "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement I' "x" "z")
|
(A "y" "z", A "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement O "x" "z")
|
(A "y" "z", E' "x" "y", O "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement O' "x" "z")
|
(A "y" "z", E' "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement O "x" "z")
|
(E "y" "z", A "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement O' "x" "z")
|
(E "y" "z", A "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement I "x" "z")
|
(E "y" "z", E' "x" "y", I "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement I' "x" "z")
|
(E "y" "z", E' "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "x" "y", Statement I "x" "z")
|
(A "y" "z", A' "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement E "x" "y", Statement O' "x" "z")
|
(A "y" "z", E "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "x" "y", Statement O "x" "z")
|
(E "y" "z", A' "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement E "x" "y", Statement I' "x" "z")
|
(E "y" "z", E "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement I "x" "y", Statement I "x" "z")
|
(A "y" "z", I "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement O' "x" "y", Statement O' "x" "z")
|
(A "y" "z", O' "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement I "x" "y", Statement O "x" "z")
|
(E "y" "z", I "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement O' "x" "y", Statement I' "x" "z")
|
(E "y" "z", O' "x" "y", I' "x" "z")
|
||||||
(Statement I "y" "z", Statement A' "x" "y", Statement I "x" "z")
|
(I "y" "z", A' "x" "y", I "x" "z")
|
||||||
(Statement I "y" "z", Statement E "x" "y", Statement O' "x" "z")
|
(I "y" "z", E "x" "y", O' "x" "z")
|
||||||
(Statement O "y" "z", Statement A' "x" "y", Statement O "x" "z")
|
(O "y" "z", A' "x" "y", O "x" "z")
|
||||||
(Statement O "y" "z", Statement E "x" "y", Statement I' "x" "z")
|
(O "y" "z", E "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement A' "x" "z")
|
(A "z" "y", A' "x" "y", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement E "x" "z")
|
(A "z" "y", E "x" "y", E "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement E "x" "z")
|
(E "z" "y", A "x" "y", E "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement A' "x" "z")
|
(E "z" "y", E' "x" "y", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement I "x" "z")
|
(A "z" "y", A' "x" "y", I "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement I' "x" "z")
|
(A "z" "y", A' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement O "x" "z")
|
(A "z" "y", E "x" "y", O "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement O' "x" "z")
|
(A "z" "y", E "x" "y", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement O "x" "z")
|
(E "z" "y", A "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement O' "x" "z")
|
(E "z" "y", A "x" "y", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement I "x" "z")
|
(E "z" "y", E' "x" "y", I "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement I' "x" "z")
|
(E "z" "y", E' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "x" "y", Statement I' "x" "z")
|
(A "z" "y", A "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E' "x" "y", Statement O "x" "z")
|
(A "z" "y", E' "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "x" "y", Statement O "x" "z")
|
(E "z" "y", A' "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement E "x" "y", Statement I' "x" "z")
|
(E "z" "y", E "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement I' "x" "y", Statement I' "x" "z")
|
(A "z" "y", I' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement O "x" "y", Statement O "x" "z")
|
(A "z" "y", O "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement I "x" "y", Statement O "x" "z")
|
(E "z" "y", I "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement O' "x" "y", Statement I' "x" "z")
|
(E "z" "y", O' "x" "y", I' "x" "z")
|
||||||
(Statement I "z" "y", Statement A' "x" "y", Statement I "x" "z")
|
(I "z" "y", A' "x" "y", I "x" "z")
|
||||||
(Statement I "z" "y", Statement E "x" "y", Statement O' "x" "z")
|
(I "z" "y", E "x" "y", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement A "x" "y", Statement O' "x" "z")
|
(O "z" "y", A "x" "y", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement E' "x" "y", Statement I "x" "z")
|
(O "z" "y", E' "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement A "x" "z")
|
(A "y" "z", A' "y" "x", A "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement E' "x" "z")
|
(A "y" "z", E' "y" "x", E' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement E "x" "z")
|
(E "y" "z", A' "y" "x", E "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement A' "x" "z")
|
(E "y" "z", E' "y" "x", A' "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement I "x" "z")
|
(A "y" "z", A' "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement I' "x" "z")
|
(A "y" "z", A' "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement O "x" "z")
|
(A "y" "z", E' "y" "x", O "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement O' "x" "z")
|
(A "y" "z", E' "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement O "x" "z")
|
(E "y" "z", A' "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement O' "x" "z")
|
(E "y" "z", A' "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement I "x" "z")
|
(E "y" "z", E' "y" "x", I "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement I' "x" "z")
|
(E "y" "z", E' "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement A "y" "x", Statement I "x" "z")
|
(A "y" "z", A "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement E "y" "x", Statement O' "x" "z")
|
(A "y" "z", E "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "y" "x", Statement O "x" "z")
|
(E "y" "z", A "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement E "y" "x", Statement I' "x" "z")
|
(E "y" "z", E "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement I "y" "x", Statement I "x" "z")
|
(A "y" "z", I "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement O "y" "x", Statement O' "x" "z")
|
(A "y" "z", O "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement I "y" "x", Statement O "x" "z")
|
(E "y" "z", I "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement O "y" "x", Statement I' "x" "z")
|
(E "y" "z", O "y" "x", I' "x" "z")
|
||||||
(Statement I "y" "z", Statement A "y" "x", Statement I "x" "z")
|
(I "y" "z", A "y" "x", I "x" "z")
|
||||||
(Statement I "y" "z", Statement E "y" "x", Statement O' "x" "z")
|
(I "y" "z", E "y" "x", O' "x" "z")
|
||||||
(Statement O "y" "z", Statement A "y" "x", Statement O "x" "z")
|
(O "y" "z", A "y" "x", O "x" "z")
|
||||||
(Statement O "y" "z", Statement E "y" "x", Statement I' "x" "z")
|
(O "y" "z", E "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement A' "x" "z")
|
(A "z" "y", A "y" "x", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement E "x" "z")
|
(A "z" "y", E "y" "x", E "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement E "x" "z")
|
(E "z" "y", A' "y" "x", E "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement A' "x" "z")
|
(E "z" "y", E' "y" "x", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement I "x" "z")
|
(A "z" "y", A "y" "x", I "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement I' "x" "z")
|
(A "z" "y", A "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement O "x" "z")
|
(A "z" "y", E "y" "x", O "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement O' "x" "z")
|
(A "z" "y", E "y" "x", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement O "x" "z")
|
(E "z" "y", A' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement O' "x" "z")
|
(E "z" "y", A' "y" "x", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement I "x" "z")
|
(E "z" "y", E' "y" "x", I "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement I' "x" "z")
|
(E "z" "y", E' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "y" "x", Statement I' "x" "z")
|
(A "z" "y", A' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E' "y" "x", Statement O "x" "z")
|
(A "z" "y", E' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A "y" "x", Statement O "x" "z")
|
(E "z" "y", A "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement E "y" "x", Statement I' "x" "z")
|
(E "z" "y", E "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement I' "y" "x", Statement I' "x" "z")
|
(A "z" "y", I' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement O' "y" "x", Statement O "x" "z")
|
(A "z" "y", O' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement I "y" "x", Statement O "x" "z")
|
(E "z" "y", I "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement O "y" "x", Statement I' "x" "z")
|
(E "z" "y", O "y" "x", I' "x" "z")
|
||||||
(Statement I "z" "y", Statement A "y" "x", Statement I "x" "z")
|
(I "z" "y", A "y" "x", I "x" "z")
|
||||||
(Statement I "z" "y", Statement E "y" "x", Statement O' "x" "z")
|
(I "z" "y", E "y" "x", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement A' "y" "x", Statement O' "x" "z")
|
(O "z" "y", A' "y" "x", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement E' "y" "x", Statement I "x" "z")
|
(O "z" "y", E' "y" "x", I "x" "z")
|
||||||
|
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
{ pkgs ? import <nixpkgs> {} }:
|
|
||||||
|
|
||||||
pkgs.mkShell {
|
|
||||||
buildInputs = with pkgs; [
|
|
||||||
ghc
|
|
||||||
];
|
|
||||||
}
|
|
||||||
Loading…
Reference in a new issue