53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder{-|

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : till@tzi.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederProvides data structures for institution comorphisms.

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski These are just collections of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- References: see Logic.hs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Todo:

5c602504f85bbac7ddf0226064452bdc7d4a8cd8Till Mossakowski Flag for model expansion property

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Weak amalgamability, also for comorphisms

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski comorphism modifications

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphisms out of sublogic relationships

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski restrictions of comorphisms to sublogics

ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowski morphisms and other translations via spans

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic.Comorphism where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maederimport Logic.Coerce

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederimport qualified Common.Lib.Set as Set

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederimport Common.Result

53310804002cd9e3c9c5844db3b984abcf001788Christian Maederimport Common.ProofUtils

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederimport Common.AS_Annotation

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederclass (Language cid,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid1 sublogics1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder | cid -> lid1, cid -> lid2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- source and target logic and sublogic

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- the target sublogic is the resulting one

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic :: cid -> sublogics2

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- finer information of target sublogics corresponding to source sublogics

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mapSublogic :: cid -> sublogics1 -> sublogics2

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- default implementation

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mapSublogic cid _ = targetSublogic cid

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- the translation functions are partial

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_theory :: cid -> (sign1,[Named sentence1])

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -> Result (sign2,[Named sentence2])

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-comorphisms

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- with no sentence translation

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- - but these are spans!

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder map_symbol :: cid -> symbol1 -> Set.Set symbol2

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents :: cid -> [String]

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski -- default implementation

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents cid = [language_name cid]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign :: Comorphism cid

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign cid sign = map_theory cid (sign,[])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign2, [Named sentence2])

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1 -> sentence1 -> m sentence2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> m (sign2, [Named sentence2])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (sign',sens') <- mapSig sign

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian Maederdata IdComorphism lid sublogics =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder IdComorphism lid sublogics

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskiinstance Logic lid sublogics

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski basic_spec sentence symb_items symb_map_items

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski Show (IdComorphism lid sublogics)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder where

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski show = language_name

933baca0720dae81434de384b32a93b47e754d09Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

586af0e9490a14dd3075095692b584c652584875Till Mossakowski Language (IdComorphism lid sublogics) where

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name (IdComorphism lid sub) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case sublogic_names lid sub of

933baca0720dae81434de384b32a93b47e754d09Christian Maeder [] -> error "language_name IdComorphism"

933baca0720dae81434de384b32a93b47e754d09Christian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

586af0e9490a14dd3075095692b584c652584875Till Mossakowski Comorphism (IdComorphism lid sublogics)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol proof_tree

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where

933baca0720dae81434de384b32a93b47e754d09Christian Maeder sourceLogic (IdComorphism lid _sub) = lid

933baca0720dae81434de384b32a93b47e754d09Christian Maeder targetLogic (IdComorphism lid _sub) = lid

933baca0720dae81434de384b32a93b47e754d09Christian Maeder sourceSublogic (IdComorphism _lid sub) = sub

933baca0720dae81434de384b32a93b47e754d09Christian Maeder targetSublogic (IdComorphism _lid sub) = sub

f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski mapSublogic _ = id

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder map_theory _ = return

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism _ = return

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_sentence _ = \_ -> return

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder map_symbol _ = Set.singleton

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents _ = []

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maederinstance (Language cid1, Language cid2)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Language (CompComorphism cid1 cid2) where

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name (CompComorphism cid1 cid2) =

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder language_name cid1++ ";" ++language_name cid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Comorphism (CompComorphism cid1 cid2)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceLogic (CompComorphism cid1 _) =

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic cid1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder targetLogic (CompComorphism _ cid2) =

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski targetLogic cid2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceSublogic (CompComorphism cid1 _) =

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic cid1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder targetSublogic (CompComorphism cid1 cid2) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic cid2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (coerceSublogic (targetLogic cid1) (sourceLogic cid2)

f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski (targetSublogic cid1))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic (CompComorphism cid1 cid2) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mapSublogic cid2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder . coerceSublogic (targetLogic cid1) (sourceLogic cid2)

f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski . mapSublogic cid1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_sentence (CompComorphism cid1 cid2) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \si1 se1 ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign cid1 si1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder se2 <- map_sentence cid1 si1 se1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (si2', se2') <- coerceBasicTheory

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (targetLogic cid1) (sourceLogic cid2)

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder "Mapping sentence along comorphism" (si2, [emptyName se2])

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case se2' of

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder [x] -> map_sentence cid2 si2' $ sentence x

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder _ -> error "CompComorphism.map_sentence"

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_theory (CompComorphism cid1 cid2) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder \ti1 ->

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder do ti2 <- map_theory cid1 ti1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder "Mapping theory along comorphism" ti2

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder map_theory cid2 ti2'

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder do m2 <- map_morphism cid1 m1

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski "Mapping signature morphism along comorphism"m2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism cid2 m3

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder in Set.unions

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (map (map_symbol cid2 . mycast)

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder (Set.toList (map_symbol cid1 s1)))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder constituents (CompComorphism cid1 cid2) =

933baca0720dae81434de384b32a93b47e754d09Christian Maeder constituents cid1 ++ constituents cid2