{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  skolemization as an institution comorphism
Copyright   :  (c) Mihai Codescu, 2016
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  codescu@iws.cs.uni-magdeburg.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Comorphism)

removing existential quantifiers from every formula
follows http://resources.mpi-inf.mpg.de/departments/rg1/teaching/autrea-ss10/script/lecture10.pdf

-}

module Comorphisms.CASL2Skolem where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic as SL hiding (bottom)
import CASL.Induction
import CASL.Quantification

import Common.Result
import Common.Id
import qualified Data.Set as Set
import Common.AS_Annotation
import Common.ProofTree
import qualified Common.Lib.MapSet as MapSet

import qualified Common.Lib.Rel as Rel

data CASL2Skolem = CASL2Skolem deriving Int -> CASL2Skolem -> ShowS
[CASL2Skolem] -> ShowS
CASL2Skolem -> String
(Int -> CASL2Skolem -> ShowS)
-> (CASL2Skolem -> String)
-> ([CASL2Skolem] -> ShowS)
-> Show CASL2Skolem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2Skolem] -> ShowS
$cshowList :: [CASL2Skolem] -> ShowS
show :: CASL2Skolem -> String
$cshow :: CASL2Skolem -> String
showsPrec :: Int -> CASL2Skolem -> ShowS
$cshowsPrec :: Int -> CASL2Skolem -> ShowS
Show

instance Language CASL2Skolem where
    language_name :: CASL2Skolem -> String
language_name CASL2Skolem = "CASL2Skolem"

instance Comorphism CASL2Skolem
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: CASL2Skolem -> CASL
sourceLogic CASL2Skolem = CASL
CASL
    sourceSublogic :: CASL2Skolem -> CASL_Sublogics
sourceSublogic CASL2Skolem = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cPrenex
    targetLogic :: CASL2Skolem -> CASL
targetLogic CASL2Skolem = CASL
CASL
    mapSublogic :: CASL2Skolem -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic CASL2Skolem sl :: CASL_Sublogics
sl = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
sl
    map_theory :: CASL2Skolem
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL2Skolem = (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory
    map_morphism :: CASL2Skolem -> CASLMor -> Result CASLMor
map_morphism CASL2Skolem = String -> CASLMor -> Result CASLMor
forall a. HasCallStack => String -> a
error "nyi"
    map_sentence :: CASL2Skolem -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence CASL2Skolem = CASLSign -> CASLFORMULA -> Result CASLFORMULA
mapSentence
    map_symbol :: CASL2Skolem -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2Skolem _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2Skolem -> Bool
has_model_expansion CASL2Skolem = Bool
True
    is_weakly_amalgamable :: CASL2Skolem -> Bool
is_weakly_amalgamable CASL2Skolem = Bool
True
    eps :: CASL2Skolem -> Bool
eps CASL2Skolem = Bool
False

mapSentence :: CASLSign -> CASLFORMULA -> Result CASLFORMULA
mapSentence :: CASLSign -> CASLFORMULA -> Result CASLFORMULA
mapSentence sig :: CASLSign
sig sen :: CASLFORMULA
sen = do
 let (_n' :: Int
_n', _nsig' :: CASLSign
_nsig', sen1 :: CASLFORMULA
sen1) = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize 0 [] CASLSign
sig CASLSign
sig CASLFORMULA
sen
 CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return CASLFORMULA
sen1  

mapTheory :: (CASLSign, [Named CASLFORMULA]) ->
          Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory (sig :: CASLSign
sig, nsens :: [Named CASLFORMULA]
nsens) = do
 let (_, nsig :: CASLSign
nsig, nsens' :: [Named CASLFORMULA]
nsens') = ((Int, CASLSign, [Named CASLFORMULA])
 -> Named CASLFORMULA -> (Int, CASLSign, [Named CASLFORMULA]))
-> (Int, CASLSign, [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> (Int, CASLSign, [Named CASLFORMULA])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(n :: Int
n, nsig0 :: CASLSign
nsig0, sens0 :: [Named CASLFORMULA]
sens0) nsen :: Named CASLFORMULA
nsen ->
        let (n' :: Int
n', nsig' :: CASLSign
nsig', sen1 :: CASLFORMULA
sen1) = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n [] CASLSign
sig CASLSign
nsig0 (CASLFORMULA -> (Int, CASLSign, CASLFORMULA))
-> CASLFORMULA -> (Int, CASLSign, CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
nsen
        in (Int
n', CASLSign
nsig', Named CASLFORMULA
nsen{sentence :: CASLFORMULA
sentence = CASLFORMULA
sen1}Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
:[Named CASLFORMULA]
sens0))
      (0, () -> CASLSign
forall e f. e -> Sign f e
emptySign (), []) [Named CASLFORMULA]
nsens
     sig' :: CASLSign
sig' = CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
sig CASLSign
nsig
 (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
sig', [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a]
reverse [Named CASLFORMULA]
nsens')

mkSkolemFunction :: Int -> Id
mkSkolemFunction :: Int -> SORT
mkSkolemFunction x :: Int
x =
 String -> SORT
genName (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ "sk_f" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x

-- replace each variable from an argument list vars
-- in a sentence sen'
-- with a new skolem function of arguments in a list fVars
-- the names are generated starting with a given number

replaceBoundVars :: [(VAR, SORT)] -> [(VAR, SORT)] -> Int -> CASLFORMULA ->
                 (CASLSign, CASLFORMULA)
replaceBoundVars :: [(VAR, SORT)]
-> [(VAR, SORT)] -> Int -> CASLFORMULA -> (CASLSign, CASLFORMULA)
replaceBoundVars vars :: [(VAR, SORT)]
vars fVars :: [(VAR, SORT)]
fVars n :: Int
n sen :: CASLFORMULA
sen = let
   -- for each variable that occurs free in sen,
   -- generate a new skolem function name
   fNames :: [SORT]
fNames = (((VAR, SORT), Int) -> SORT) -> [((VAR, SORT), Int)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SORT
mkSkolemFunction (Int -> SORT)
-> (((VAR, SORT), Int) -> Int) -> ((VAR, SORT), Int) -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VAR, SORT), Int) -> Int
forall a b. (a, b) -> b
snd) ([((VAR, SORT), Int)] -> [SORT]) -> [((VAR, SORT), Int)] -> [SORT]
forall a b. (a -> b) -> a -> b
$ [(VAR, SORT)] -> [Int] -> [((VAR, SORT), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(VAR, SORT)]
fVars ([Int] -> [((VAR, SORT), Int)]) -> [Int] -> [((VAR, SORT), Int)]
forall a b. (a -> b) -> a -> b
$ [Int
n..]
   -- for each such name, its arguments will be the types of vars
   -- and the result, the corresponding sort in fVars
   otypes :: [OP_TYPE]
otypes = (SORT -> OP_TYPE) -> [SORT] -> [OP_TYPE]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: SORT
x -> OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total (((VAR, SORT) -> SORT) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd [(VAR, SORT)]
vars) SORT
x Range
nullRange) ([SORT] -> [OP_TYPE]) -> [SORT] -> [OP_TYPE]
forall a b. (a -> b) -> a -> b
$
             ((VAR, SORT) -> SORT) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd [(VAR, SORT)]
fVars
   -- now create the operation symbols with names in fNames and arity in otypes
   osyms :: [OP_SYMB]
osyms = ((SORT, OP_TYPE) -> OP_SYMB) -> [(SORT, OP_TYPE)] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: SORT
x, y :: OP_TYPE
y) -> SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
x OP_TYPE
y Range
nullRange) ([(SORT, OP_TYPE)] -> [OP_SYMB]) -> [(SORT, OP_TYPE)] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$
            [SORT] -> [OP_TYPE] -> [(SORT, OP_TYPE)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SORT]
fNames [OP_TYPE]
otypes
   -- the arguments are the outer variables
   args :: [TERM f]
args = ((VAR, SORT) -> TERM f) -> [(VAR, SORT)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\(v :: VAR
v,s :: SORT
s) -> VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
nullRange) [(VAR, SORT)]
vars
   -- now create the term gn_sk_k(outerVariables)
   tms :: [TERM f]
tms = (OP_SYMB -> TERM f) -> [OP_SYMB] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\os :: OP_SYMB
os -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os [TERM f]
forall f. [TERM f]
args Range
nullRange) [OP_SYMB]
osyms
   substs :: [(VAR, SORT, TERM f)]
substs = (((VAR, SORT), TERM f) -> (VAR, SORT, TERM f))
-> [((VAR, SORT), TERM f)] -> [(VAR, SORT, TERM f)]
forall a b. (a -> b) -> [a] -> [b]
map (\((a :: VAR
a,b :: SORT
b),c :: TERM f
c) -> (VAR
a,SORT
b,TERM f
c)) ([((VAR, SORT), TERM f)] -> [(VAR, SORT, TERM f)])
-> [((VAR, SORT), TERM f)] -> [(VAR, SORT, TERM f)]
forall a b. (a -> b) -> a -> b
$ [(VAR, SORT)] -> [TERM f] -> [((VAR, SORT), TERM f)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(VAR, SORT)]
fVars [TERM f]
forall f. [TERM f]
tms
   sen' :: CASLFORMULA
sen' = (CASLFORMULA -> (VAR, SORT, TERM ()) -> CASLFORMULA)
-> CASLFORMULA -> [(VAR, SORT, TERM ())] -> CASLFORMULA
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\f :: CASLFORMULA
f (v :: VAR
v,s :: SORT
s,t :: TERM ()
t)-> VAR -> SORT -> TERM () -> CASLFORMULA -> CASLFORMULA
forall f.
FormExtension f =>
VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute VAR
v SORT
s TERM ()
t CASLFORMULA
f) CASLFORMULA
sen [(VAR, SORT, TERM ())]
forall f. [(VAR, SORT, TERM f)]
substs
   sign' :: Sign f ()
sign' = (() -> Sign f ()
forall e f. e -> Sign f e
emptySign ()) {
               sortRel :: Rel SORT
sortRel = (Rel SORT -> SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\r :: Rel SORT
r x :: SORT
x -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
x Rel SORT
r) Rel SORT
forall a. Rel a
Rel.empty ([SORT] -> Rel SORT) -> [SORT] -> Rel SORT
forall a b. (a -> b) -> a -> b
$
                         ((VAR, SORT) -> SORT) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd  ([(VAR, SORT)] -> [SORT]) -> [(VAR, SORT)] -> [SORT]
forall a b. (a -> b) -> a -> b
$ [(VAR, SORT)]
vars [(VAR, SORT)] -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. [a] -> [a] -> [a]
++ [(VAR, SORT)]
fVars,
               opMap :: OpMap
opMap = (OpMap -> (SORT, OP_TYPE) -> OpMap)
-> OpMap -> [(SORT, OP_TYPE)] -> OpMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m :: OpMap
m (f :: SORT
f,o :: OP_TYPE
o) -> SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
f (OP_TYPE -> OpType
toOpType OP_TYPE
o) OpMap
m)
                       OpMap
forall a b. MapSet a b
MapSet.empty ([(SORT, OP_TYPE)] -> OpMap) -> [(SORT, OP_TYPE)] -> OpMap
forall a b. (a -> b) -> a -> b
$ [SORT] -> [OP_TYPE] -> [(SORT, OP_TYPE)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SORT]
fNames [OP_TYPE]
otypes
            }
  in (CASLSign
forall f. Sign f ()
sign', CASLFORMULA
sen')

-- skolemization:
-- exists x H =>
-- H(f(y_1,...,y_n)/x)
-- where y_1, ..., y_n are free in exists x H
-- f is a new function symbol of arity n
skolemize :: Int -> [(VAR, SORT)] -> CASLSign -> CASLSign -> CASLFORMULA ->
             (Int, CASLSign, CASLFORMULA)
skolemize :: Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize n :: Int
n outerFreeVars :: [(VAR, SORT)]
outerFreeVars osig :: CASLSign
osig nsig :: CASLSign
nsig sen :: CASLFORMULA
sen = case CASLFORMULA
sen of
 Quantification Existential vdecls :: [VAR_DECL]
vdecls sen1 :: CASLFORMULA
sen1 _ -> let
   vars :: [(VAR, SORT)]
vars = [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
vdecls
   (n' :: Int
n', nsig' :: CASLSign
nsig', sen' :: CASLFORMULA
sen') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n [(VAR, SORT)]
outerFreeVars CASLSign
osig CASLSign
nsig CASLFORMULA
sen1
   --fVars = freeVars osig sen'
   n'' :: Int
n'' =  Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ([(VAR, SORT)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(VAR, SORT)]
vars)
   (nsig0 :: CASLSign
nsig0, sen'' :: CASLFORMULA
sen'') = [(VAR, SORT)]
-> [(VAR, SORT)] -> Int -> CASLFORMULA -> (CASLSign, CASLFORMULA)
replaceBoundVars [(VAR, SORT)]
outerFreeVars [(VAR, SORT)]
vars Int
n CASLFORMULA
sen'
   nsig'' :: CASLSign
nsig'' = CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
nsig' CASLSign
nsig0
  in (Int
n'', CASLSign
nsig'', CASLFORMULA
sen'')
 Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars sen1 :: CASLFORMULA
sen1 _ ->
   let (n' :: Int
n', nsig' :: CASLSign
nsig', sen' :: CASLFORMULA
sen') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n ([(VAR, SORT)]
outerFreeVars [(VAR, SORT)] -> [(VAR, SORT)] -> [(VAR, SORT)]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs [VAR_DECL]
vars)
                           CASLSign
osig CASLSign
nsig CASLFORMULA
sen1
   in (Int
n', CASLSign
nsig', QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars CASLFORMULA
sen' Range
nullRange)
 Junction j :: Junctor
j sens :: [CASLFORMULA]
sens _ -> let
   (n' :: Int
n', nsig' :: CASLSign
nsig', sens' :: [CASLFORMULA]
sens') = ((Int, CASLSign, [CASLFORMULA])
 -> CASLFORMULA -> (Int, CASLSign, [CASLFORMULA]))
-> (Int, CASLSign, [CASLFORMULA])
-> [CASLFORMULA]
-> (Int, CASLSign, [CASLFORMULA])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(x :: Int
x, nsig0 :: CASLSign
nsig0, sens0 :: [CASLFORMULA]
sens0) s :: CASLFORMULA
s ->
      let (y :: Int
y, nsig1 :: CASLSign
nsig1, s' :: CASLFORMULA
s') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
x [(VAR, SORT)]
outerFreeVars CASLSign
osig CASLSign
nsig0 CASLFORMULA
s
      in (Int
y, CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
nsig1 CASLSign
nsig0, CASLFORMULA
s'CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
:[CASLFORMULA]
sens0))
                        (Int
n, CASLSign
nsig, []) [CASLFORMULA]
sens
  in (Int
n', CASLSign
nsig', Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ([CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a]
reverse [CASLFORMULA]
sens') Range
nullRange)
 Relation sen1 :: CASLFORMULA
sen1 rel :: Relation
rel sen2 :: CASLFORMULA
sen2 _ -> let
   (n' :: Int
n', nsig' :: CASLSign
nsig', sen' :: CASLFORMULA
sen') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n [(VAR, SORT)]
outerFreeVars CASLSign
osig CASLSign
nsig CASLFORMULA
sen1
   (n'' :: Int
n'', nsig'' :: CASLSign
nsig'', sen'' :: CASLFORMULA
sen'') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n' [(VAR, SORT)]
outerFreeVars CASLSign
osig CASLSign
nsig' CASLFORMULA
sen2
  in (Int
n'', CASLSign
nsig'', CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen' Relation
rel CASLFORMULA
sen'' Range
nullRange)
 Negation sen1 :: CASLFORMULA
sen1 _ ->
  let (n' :: Int
n', nsig' :: CASLSign
nsig', sen' :: CASLFORMULA
sen') = Int
-> [(VAR, SORT)]
-> CASLSign
-> CASLSign
-> CASLFORMULA
-> (Int, CASLSign, CASLFORMULA)
skolemize Int
n [(VAR, SORT)]
outerFreeVars CASLSign
osig CASLSign
nsig CASLFORMULA
sen1
  in (Int
n', CASLSign
nsig', CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen' Range
nullRange)
 x :: CASLFORMULA
x -> (Int
n, CASLSign
nsig, CASLFORMULA
x)