66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedertype Nat

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maederops 0, 1 : Nat

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederops __+__, __-__, min : Nat * Nat -> Nat

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederpreds __>=__, __<=__, __>__ : Nat * Nat

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederfree type Boolean ::= True | False

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedervars S, V : Type

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maedertype Set S := S ->? Unit

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederops emptySet : Set S;

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder {__} : S -> Set S;

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder __isIn__ : S * Set S ->? Unit;

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder __subset__ : Pred (Set (S) * Set (S));

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder __union__, __intersection__, __\\__ : Set S * Set S -> Set S;

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder __disjoint__ : Pred (Set (S) * Set (S));

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder __*__ : Set S * Set V -> Set (S * V);

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder __disjointUnion__ : Set S * Set S -> Set (S * Boolean);

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder injl, injr : S -> S * Boolean

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedervar Elem : Type

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maedertype MultiSet Elem := Elem ->? Nat

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederops __isIn__ : Pred (Elem * MultiSet Elem);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __<=__ : Pred (MultiSet Elem * MultiSet Elem);

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder {} : MultiSet Elem;

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder {__} : Elem -> MultiSet Elem;

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder __+__, __-__, __intersection__

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder : MultiSet Elem * MultiSet Elem -> MultiSet Elem;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder freq : Elem * MultiSet Elem -> Nat;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder setToMultiSet : Set Elem -> MultiSet Elem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedervar Elem : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederop MultiSetToSet : MultiSet Elem -> Set Elem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederforall B : MultiSet Elem; S : Set Elem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder. let S = MultiSetToSet B in

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder forall x : Elem . x isIn S <=> freq (x, B) > 0;

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedervar S : Type

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedertype MapMultiSet S := MultiSet S ->? MultiSet S

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedervar a : Type

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederops sumN : (Nat ->? Nat) -> Nat -> Nat;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sumSet : Set Nat ->? Nat;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder sum : (a ->? Nat) -> Pred a ->? Nat

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maedervars S, V, U : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype Map S := S ->? S

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederops dom : (S ->? V) -> Set S;

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder range : (S ->? V) -> Set V;

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder image : (S ->? V) -> Set S -> Set V;

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder emptyMap : (S ->? V);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __[__/__] : (S ->? V) * S * V -> (S ->? V);

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder __-__ : (S ->? V) * S -> (S ->? V);

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder __o__ : (V ->? U) * (S ->? V) -> (S ->? U);

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder __||__ : (S ->? V) * Set S -> (S ->? V);

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder undef__ : S ->? V;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ker : (S ->? V) -> Pred (S * S);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder injective : Pred (S ->? V);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __intersectionMap__, __unionMap__

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder : (S ->? V) * (S ->? V) -> (S ->? V);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __restrict__ : (S ->? V) * Set S -> (S ->? V)

07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maedervars S, V : Type

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederops __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder freeMap : Map S -> MapMultiSet S;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederop __intersection__

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder : MultiSet Elem * MultiSet Elem -> MultiSet Elem, assoc, comm, idem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertypes P, T

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype Net =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {(p, pre, post) : Set P * (T ->? MultiSet P) * (T ->? MultiSet P)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder . (dom pre = dom post

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder /\ forall p1 : MultiSet P

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . p1 isIn range pre => MultiSetToSet p1 subset p)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder /\ forall p1 : MultiSet P

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . p1 isIn range pre => MultiSetToSet p1 subset p

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederops places : Net -> Set P;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder transitions : Net -> Set T;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder preMap, postMap : Net -> (T ->? MultiSet P)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype HomNet =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {(n1, hp, ht, n2) : Net * (P ->? P) * (T ->? T) * Net

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . hp :: places n1 --> places n2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder /\ ht :: transitions n1 --> transitions n2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder /\ forall t : T

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . t isIn transitions n1

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder => freeMap hp (preMap n1 t) = preMap n2 (ht t)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder /\ freeMap hp (postMap n1 t) = postMap n2 (ht t)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederops dom : HomNet -> Net;

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder cod : HomNet -> Net;

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder placesMap : HomNet -> (P ->? P);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder transitionsMap : HomNet -> (T ->? T);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id : Net ->? HomNet;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __o__ : HomNet * HomNet ->? HomNet

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederpred injective : HomNet

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype Marking := MultiSet P

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertype System =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {(n, m) : Net * Marking

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . let (p, pre1, post1) = n in forall x : P . x isIn m => x isIn p

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederops marking : System -> Marking;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder net : System -> Net;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder empty : Marking;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __|<__> : System * T -> System;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __|<__> : System * MultiSet T ->? System

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maedertype HomSys =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {(sys1, hp, ht, sys2) : System * (P ->? P) * (T ->? T) * System

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . ((net sys1, hp, ht, net sys2) in HomNet)

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder /\ forall p : P

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder . freq (p, marking sys1) <= freq (hp p, marking sys2)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederops dom : HomSys -> System;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cod : HomSys -> System;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder placesMap : HomSys -> (P ->? P);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder transitionsMap : HomSys -> (T ->? T);

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder id : System ->? HomSys;

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder __o__ : HomSys * HomSys ->? HomSys

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederpred injective : HomSys

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederforall h1, h2 : HomSys

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder. def (h2 o h1)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder => h2 o h1

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder = ((dom h1, placesMap h2 o placesMap h1,

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder transitionsMap h2 o transitionsMap h1, cod h2)

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder as HomSys);

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder%% Type Constructors -----------------------------------------------------

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederBoolean : Type %[free type Boolean ::= False | True]%

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederHomNet : Type := _t1015 Net

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederHomSys : Type := _t1513 System

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederMap : Type -> Type := \ S : Type . S ->? S

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederMapMultiSet

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder: Type -> Type := \ S : Type . MultiSet S ->? MultiSet S

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederMarking : Type := MultiSet P

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederMultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederNat : Type

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederNet : Type := _t364 (T ->? MultiSet P)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederP : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederSet : Type -> Type := \ S : Type . S ->? Unit

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederSystem : Type := _t1087 Marking

61091743da1a9ed6dfd5e077fdcc972553358962Christian MaederT : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1015 : +Type -> Type := _t1016 (T ->? T)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1016 : +Type -> +Type -> Type := _t1017 (P ->? P)

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder_t1017 : +Type -> +Type -> +Type -> Type := _t1018 Net

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1018 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder_t1087 : +Type -> Type := _t1088 Net

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1088 : +Type -> +Type -> Type < __*__

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1513 : +Type -> Type := _t1514 (T ->? T)

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder_t1514 : +Type -> +Type -> Type := _t1515 (P ->? P)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t1515 : +Type -> +Type -> +Type -> Type := _t1516 System

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder_t1516 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder_t364 : +Type -> Type := _t365 (T ->? MultiSet P)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t365 : +Type -> +Type -> Type := _t366 (Set P)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder_t366 : +Type -> +Type -> +Type -> Type < __*__*__

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%% Type Variables --------------------------------------------------------

76647324ed70f33b95a881b536d883daccf9568dChristian MaederElem : Type %(var_6)%

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederS : Type %(var_62)%

76647324ed70f33b95a881b536d883daccf9568dChristian MaederU : Type %(var_60)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederV : Type %(var_63)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedera : Type %(var_57)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%% Assumptions -----------------------------------------------------------

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder0 : Nat %(op)%

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder1 : Nat %(op)%

405b95208385572f491e1e0207d8d14e31022fa6Christian MaederFalse : Boolean %(constructor)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederMultiSetToSet : forall Elem : Type . MultiSet Elem -> Set Elem

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederTrue : Boolean %(constructor)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__*__ : forall S : Type; V : Type . Set S * Set V -> Set (S * V)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__+__ : Nat * Nat -> Nat %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__+__ : forall Elem : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . MultiSet Elem * MultiSet Elem -> MultiSet Elem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__-__ : Nat * Nat -> Nat %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__-__ : forall Elem : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . MultiSet Elem * MultiSet Elem -> MultiSet Elem

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__-__ : forall S : Type; V : Type . (S ->? V) * S -> S ->? V %(op)%

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder__::__-->__ : forall S : Type; V : Type

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder . Pred ((S ->? V) * Pred S * Pred V)

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__::__-->__ : forall S : Type; V : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . Pred ((S ->? MultiSet V) * Set S * Set V)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__<=__ : Nat * Nat ->? Unit %(pred)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__<=__ : forall Elem : Type . Pred (MultiSet Elem * MultiSet Elem)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(op)%

341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder__>__ : Nat * Nat ->? Unit %(pred)%

341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder__>=__ : Nat * Nat ->? Unit %(pred)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder__[__/__] : forall S : Type; V : Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder . (S ->? V) * S * V -> S ->? V

%(op)%

__\\__ : forall S : Type . Set S * Set S -> Set S %(op)%

__disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%

__disjointUnion__ : forall S : Type

. Set S * Set S -> Set (S * Boolean)

%(op)%

__intersection__ : forall Elem : Type

. MultiSet Elem * MultiSet Elem -> MultiSet Elem,

assoc, comm, idem %(op)%

__intersection__ : forall S : Type . Set S * Set S -> Set S %(op)%

__intersectionMap__ : forall S : Type; V : Type

. (S ->? V) * (S ->? V) -> S ->? V

%(op)%

__isIn__ : forall S : Type . S * Set S ->? Unit %(op)%

__isIn__ : forall Elem : Type . Pred (Elem * MultiSet Elem) %(op)%

__o__ : HomNet * HomNet ->? HomNet %(op)%

__o__ : HomSys * HomSys ->? HomSys %(op)%

__o__ : forall S : Type; V : Type; U : Type

. (V ->? U) * (S ->? V) -> S ->? U

%(op)%

__restrict__ : forall S : Type; V : Type

. (S ->? V) * Set S -> S ->? V

%(op)%

__subset__ : forall S : Type . Pred (Set S * Set S) %(op)%

__union__ : forall S : Type . Set S * Set S -> Set S %(op)%

__unionMap__ : forall S : Type; V : Type

. (S ->? V) * (S ->? V) -> S ->? V

%(op)%

__|<__> : System * T -> System %(op)%

__|<__> : System * MultiSet T ->? System %(op)%

__||__ : forall S : Type; V : Type . (S ->? V) * Set S -> S ->? V

%(op)%

cod : HomNet -> Net %(op)%

cod : HomSys -> System %(op)%

dom : HomNet -> Net %(op)%

dom : HomSys -> System %(op)%

dom : forall S : Type; V : Type . (S ->? V) -> Set S %(op)%

empty : Marking %(op)%

emptyMap : forall S : Type; V : Type . S ->? V %(op)%

emptySet : forall S : Type . Set S %(op)%

freeMap : forall S : Type . Map S -> MapMultiSet S %(op)%

freq : forall Elem : Type . Elem * MultiSet Elem -> Nat %(op)%

id : System ->? HomSys %(op)%

id : Net ->? HomNet %(op)%

image : forall S : Type; V : Type . (S ->? V) -> Set S -> Set V

%(op)%

injective : HomNet ->? Unit %(pred)%

injective : HomSys ->? Unit %(pred)%

injective : forall S : Type; V : Type . Pred (S ->? V) %(op)%

injl : forall S : Type . S -> S * Boolean %(op)%

injr : forall S : Type . S -> S * Boolean %(op)%

ker : forall S : Type; V : Type . (S ->? V) -> Pred (S * S) %(op)%

linMap : forall S : Type; V : Type

. (S ->? MultiSet V) -> MultiSet S ->? MultiSet V

%(op)%

marking : System -> Marking %(op)%

min : Nat * Nat -> Nat %(op)%

net : System -> Net %(op)%

places : Net -> Set P %(op)%

placesMap : HomNet -> P ->? P %(op)%

placesMap : HomSys -> P ->? P %(op)%

postMap : Net -> T ->? MultiSet P %(op)%

preMap : Net -> T ->? MultiSet P %(op)%

range : forall S : Type; V : Type . (S ->? V) -> Set V %(op)%

setToMultiSet : forall Elem : Type . Set Elem -> MultiSet Elem

%(op)%

sum : forall a : Type . (a ->? Nat) -> Pred a ->? Nat %(op)%

sumN : (Nat ->? Nat) -> Nat -> Nat %(op)%

sumSet : Set Nat ->? Nat %(op)%

transitions : Net -> Set T %(op)%

transitionsMap : HomNet -> T ->? T %(op)%

transitionsMap : HomSys -> T ->? T %(op)%

undef__ : forall S : Type; V : Type . S ->? V %(op)%

{__} : forall Elem : Type . Elem -> MultiSet Elem %(op)%

{__} : forall S : Type . S -> Set S %(op)%

{} : forall Elem : Type . MultiSet Elem %(op)%

%% Variables -------------------------------------------------------------

B : MultiSet Elem

S : Set Elem

h1 : HomSys

h2 : HomSys

%% Sentences -------------------------------------------------------------

free type Boolean ::= False | True %(ga_Boolean)%

let S = MultiSetToSet B in

forall x : Elem

. (__isIn__ : Elem * Set Elem ->? Unit) (x, S) <=> freq (x, B) > 0

def (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)

=> (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)

= (((op dom : HomSys -> System) h1,

(__o__ : (P ->? P) * (P ->? P) -> P ->? P)

((op placesMap : HomSys -> P ->? P) h2,

(op placesMap : HomSys -> P ->? P) h1),

(__o__ : (T ->? T) * (T ->? T) -> T ->? T)

((op transitionsMap : HomSys -> T ->? T) h2,

(op transitionsMap : HomSys -> T ->? T) h1),

(op cod : HomSys -> System) h2)

as HomSys)

%% Diagnostics -----------------------------------------------------------

### Hint 7.7, is type variable 'S'

### Hint 7.9, is type variable 'V'

### Hint 19.7, is type variable 'Elem'

### Hint 31.6, is type variable 'Elem'

### Hint 31.6, rebound type variable 'Elem'

### Hint 33.10, not a kind 'MultiSet Elem'

### Hint 33.27, not a kind 'Set Elem'

### Hint 35.17, not a class 'Elem'

### Hint 34.12, rebound variable 'S'

### Hint 34.12, rebound variable 'S'

### Hint, rejected 'Unit < Nat' of '((var x : Elem), (var S : Set Elem))'

### Hint 35.25-35.32, untypable term (with type: _v21_Elem * MultiSet _v21_Elem)

'(x, S)'

### Hint 37.7, is type variable 'S'

### Hint 37.7, rebound type variable 'S'

### Hint 40.7, is type variable 'a'

### Hint 45.7, is type variable 'S'

### Hint 45.7, rebound type variable 'S'

### Hint 45.9, is type variable 'V'

### Hint 45.9, rebound type variable 'V'

### Hint 45.11, is type variable 'U'

### Hint 62.7, is type variable 'S'

### Hint 62.7, rebound type variable 'S'

### Hint 62.10, is type variable 'V'

### Hint 62.10, rebound type variable 'V'

### Hint 67.10, repeated declaration of '__intersection__'

### Hint 72.23, not a kind 'MultiSet P'

### Hint 73.26, not a kind 'MultiSet P'

### Hint 72.45, rejected 'Unit < Nat' of '((var p1 : MultiSet P),

(op range : forall S : Type; V : Type . (S ->? V) -> Set V)

(var pre : T ->? MultiSet P))'

### Hint 72.37-72.51, untypable term (with type: _v142_Elem * MultiSet _v142_Elem)

'(p1, range pre)'

### Hint 73.48, rejected 'Unit < Nat' of '((var p1 : MultiSet P),

(op range : forall S : Type; V : Type . (S ->? V) -> Set V)

(var pre : T ->? MultiSet P))'

### Hint 73.40-73.54, untypable term (with type: _v257_Elem * MultiSet _v257_Elem)

'(p1, range pre)'

### Hint 81.19, not a class 'T'

### Hint 80.14-80.35, in type of '((var hp : P ->? P), (op places : Net -> Set P) (var n1 : Net),

(op places : Net -> Set P) (var n2 : Net))'

typename 'P' (79.35)

is not unifiable with type '_v383_V ->? Nat' (63.47)

### Hint 80.8-80.35, untypable term (with type: (_v382_S ->? MultiSet _v383_V) * Set _v382_S * Set _v383_V)

'(hp, places n1, places n2)'

### Hint 80.47-80.78, in type of '((var ht : T ->? T),

(op transitions : Net -> Set T) (var n1 : Net),

(op transitions : Net -> Set T) (var n2 : Net))'

typename 'T' (79.45)

is not unifiable with type '_v557_V ->? Nat' (63.47)

### Hint 80.41-80.78, untypable term (with type: (_v556_S ->? MultiSet _v557_V) * Set _v556_S * Set _v557_V)

'(ht, transitions n1, transitions n2)'

### Hint 81.31, rejected 'Unit < Nat' of '((var t : T), (op transitions : Net -> Set T) (var n1 : Net))'

### Hint 81.24-81.43, untypable term (with type: _v734_Elem * MultiSet _v734_Elem)

'(t, transitions n1)'

### Hint 95.38, not a class 'P'

### Hint, rejected 'Nat < Unit' of '((var x : P), (var m : Marking))'

### Hint 95.43-95.50, untypable term (with type: _v1049_S * Set _v1049_S)

'(x, m)'

### Hint 94.29-95.62, rejected 'Unit < Nat' of 'let ((var p : _v1024 _v1025 _v1023),

(var pre1 : _v1028 _v1029 (_v1032 _v1033 _v1031)),

(var post1 : _v1036 _v1037 (_v1040 _v1041 _v1039)))

= (var n : Net)

in

forall x : P

. ((op __isIn__ : forall Elem : Type . Pred (Elem * MultiSet Elem))

((var x : P), (var m : Marking)))

=> ((op __isIn__ :

forall Elem : Type . Pred (Elem * MultiSet Elem))

((var x : P), (var p : _v1024 _v1025 _v1023)))'

### Hint 104.19, not a class 'P'

### Hint 104.24-104.74, in type of '((op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)

((var p : P),

(op marking : System -> Marking) (var sys1 : System)),

(op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)

((var hp : P ->? P) (var p : P),

(op marking : System -> Marking) (var sys2 : System)))'

typename 'Nat' (28.38)

is not unifiable with type '_v1288_Elem ->? Nat' (23.33)

### Hint 104.24-104.74, untypable term (with type: MultiSet _v1288_Elem * MultiSet _v1288_Elem)

'(freq (p, marking sys1), freq (hp p, marking sys2))'

### Hint 112.12, not a class 'HomSys'

### Hint 112.16, not a class 'HomSys'

### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 113.10-113.15, untypable term (with type: HomNet * HomNet)

'(h2, h1)'

### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1515 (P ->? P)' (102.54)

### Hint 113.10-113.15, untypable term (with type: (_v1526_V ->? _v1527_U) * (_v1528_S ->? _v1526_V))

'(h2, h1)'

### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 113.22-113.27, untypable term (with type: HomNet * HomNet)

'(h2, h1)'

### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1515 (P ->? P)' (102.54)

### Hint 113.22-113.27, untypable term (with type: (_v2102_V ->? _v2103_U) * (_v2104_S ->? _v2102_V))

'(h2, h1)'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.11, untypable term (with type: HomNet)

'h1'

### Hint, in type of '(var h1 : HomSys)'

typename '__->?__'

is not unifiable with type '_t1515 (P ->? P)' (102.54)

### Hint 114.11, untypable term (with type: _v2588_S ->? _v2589_V)

'h1'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.25, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.40, untypable term (with type: HomNet)

'h1'

### Hint 114.15-114.40, in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),

(op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1017 (P ->? P)' (79.35)

### Hint 114.15-114.40, untypable term (with type: HomNet * HomNet)

'(placesMap h2, placesMap h1)'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.25, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.40, untypable term (with type: HomNet)

'h1'

### Hint 114.15-114.40, in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),

(op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1515 (P ->? P)' (102.54)

### Hint 114.15-114.40, untypable term (with type: HomSys * HomSys)

'(placesMap h2, placesMap h1)'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.25, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.40, untypable term (with type: HomNet)

'h1'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.59, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.79, untypable term (with type: HomNet)

'h1'

### Hint 114.44-114.79, in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),

(op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1017 (P ->? P)' (79.35)

### Hint 114.44-114.79, untypable term (with type: HomNet * HomNet)

'(transitionsMap h2, transitionsMap h1)'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.59, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.79, untypable term (with type: HomNet)

'h1'

### Hint 114.44-114.79, in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),

(op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'

typename '__->?__'

is not unifiable with type '_t1515 (P ->? P)' (102.54)

### Hint 114.44-114.79, untypable term (with type: HomSys * HomSys)

'(transitionsMap h2, transitionsMap h1)'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.59, untypable term (with type: HomNet)

'h2'

### Hint, in type of '(var h1 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.79, untypable term (with type: HomNet)

'h1'

### Hint, in type of '(var h2 : HomSys)'

typename '_t1088' (93.8)

is not unifiable with type '_t366 (Set P)' (71.34)

### Hint 114.86, untypable term (with type: HomNet)

'h2'