abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedertype Nat

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederops 0, 1 : Nat

09249711700a6acbc40a2e337688b434d7aafa28Christian Maederops __+__, __-__, min : Nat * Nat -> Nat

76647324ed70f33b95a881b536d883daccf9568dChristian Maederpreds __>=__, __<=__, __>__ : Nat * Nat

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederfree type Boolean ::= True | False

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedervars S, V : Type

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maedertype Set S := S ->? Unit

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederops emptySet : Set S;

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder {__} : S -> Set S;

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

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

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

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

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

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

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

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedervar Elem : Type

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maedertype MultiSet Elem := Elem ->? Nat

0a39036fa485579a7b7c81cdd44a412392571927Christian Maederops __isIn__ : Pred (Elem * MultiSet Elem);

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

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder {} : MultiSet Elem;

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

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder __+__, __-__, __intersection__

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

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder freq : Elem * MultiSet Elem -> Nat;

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder setToMultiSet : Set Elem -> MultiSet Elem

d48085f765fca838c1d972d2123601997174583dChristian Maedervar Elem : Type

76647324ed70f33b95a881b536d883daccf9568dChristian Maederop MultiSetToSet : MultiSet Elem -> Set Elem

d48085f765fca838c1d972d2123601997174583dChristian Maederforall B : MultiSet Elem; S : Set Elem

d48085f765fca838c1d972d2123601997174583dChristian Maeder. let S = MultiSetToSet B in

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

d48085f765fca838c1d972d2123601997174583dChristian Maedervar S : Type

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

d48085f765fca838c1d972d2123601997174583dChristian Maedervar a : Type

d48085f765fca838c1d972d2123601997174583dChristian Maederops sumN : (Nat ->? Nat) -> Nat -> Nat;

d48085f765fca838c1d972d2123601997174583dChristian Maeder sumSet : Set Nat ->? Nat;

d48085f765fca838c1d972d2123601997174583dChristian Maeder sum : (a ->? Nat) -> Pred a ->? Nat

d48085f765fca838c1d972d2123601997174583dChristian Maedervars S, V, U : Type

a39a820684c1974350f46593025e0bb279f41bc6Christian Maedertype Map S := S ->? S

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

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

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

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

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

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

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

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

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder undef__ : S ->? V;

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder injective : Pred (S ->? V);

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder __intersectionMap__, __unionMap__

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder : (S ->? V) * (S ->? V) -> (S ->? V);

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder __restrict__ : (S ->? V) * Set S -> (S ->? V)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maedervars S, V : Type

2143841e2b81aa0eaafa6bf81eb57cef33cf29e6Christian Maederops __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder freeMap : Map S -> MapMultiSet S;

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maederop __intersection__

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder : MultiSet Elem * MultiSet Elem -> MultiSet Elem, assoc, comm, idem

793945d4ac7c0f22760589c87af8e71427c76118Christian Maedertypes P, T

793945d4ac7c0f22760589c87af8e71427c76118Christian Maedertype Net =

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder . (dom pre = dom post

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder /\ forall p1 : MultiSet P

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder . p1 isIn range pre => MultiSetToSet p1 subset p)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder /\ forall p1 : MultiSet P

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder . p1 isIn range pre => MultiSetToSet p1 subset p

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder }

793945d4ac7c0f22760589c87af8e71427c76118Christian Maederops places : Net -> Set P;

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder transitions : Net -> Set T;

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder preMap, postMap : Net -> (T ->? MultiSet P)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maedertype HomNet =

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder . hp :: places n1 --> places n2

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder /\ ht :: transitions n1 --> transitions n2

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder /\ forall t : T

d48085f765fca838c1d972d2123601997174583dChristian Maeder . t isIn transitions n1

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder => freeMap hp (preMap n1 t) = preMap n2 (ht t)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder /\ freeMap hp (postMap n1 t) = postMap n2 (ht t)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder }

793945d4ac7c0f22760589c87af8e71427c76118Christian Maederops dom : HomNet -> Net;

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder cod : HomNet -> Net;

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder placesMap : HomNet -> (P ->? P);

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder transitionsMap : HomNet -> (T ->? T);

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder id : Net ->? HomNet;

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder __o__ : HomNet * HomNet ->? HomNet

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maederpred injective : HomNet

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maedertype Marking := MultiSet P

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maedertype System =

d48085f765fca838c1d972d2123601997174583dChristian Maeder {(n, m) : Net * Marking

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder }

d48085f765fca838c1d972d2123601997174583dChristian Maederops marking : System -> Marking;

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder net : System -> Net;

d48085f765fca838c1d972d2123601997174583dChristian Maeder empty : Marking;

d48085f765fca838c1d972d2123601997174583dChristian Maeder __|<__> : System * T -> System;

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder __|<__> : System * MultiSet T ->? System

d48085f765fca838c1d972d2123601997174583dChristian Maedertype HomSys =

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

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder /\ forall p : P

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder }

d48085f765fca838c1d972d2123601997174583dChristian Maederops dom : HomSys -> System;

d48085f765fca838c1d972d2123601997174583dChristian Maeder cod : HomSys -> System;

d48085f765fca838c1d972d2123601997174583dChristian Maeder placesMap : HomSys -> (P ->? P);

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder id : System ->? HomSys;

d48085f765fca838c1d972d2123601997174583dChristian Maeder __o__ : HomSys * HomSys ->? HomSys

d48085f765fca838c1d972d2123601997174583dChristian Maederpred injective : HomSys

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederforall h1, h2 : HomSys

d48085f765fca838c1d972d2123601997174583dChristian Maeder. def (h2 o h1)

d48085f765fca838c1d972d2123601997174583dChristian Maeder => h2 o h1

d48085f765fca838c1d972d2123601997174583dChristian Maeder = ((dom h1, placesMap h2 o placesMap h1,

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

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder as HomSys);

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maedertypes

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederBoolean : Type %[free type Boolean ::= False | True]%;

d48085f765fca838c1d972d2123601997174583dChristian MaederHomNet : Type := _t935 Net;

d48085f765fca838c1d972d2123601997174583dChristian MaederHomSys : Type := _t1433 System;

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederMap : Type -> Type := \ S : Type . S ->? S;

d48085f765fca838c1d972d2123601997174583dChristian MaederMapMultiSet

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder: Type -> Type := \ S : Type . MultiSet S ->? MultiSet S;

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederMarking : Type := MultiSet P;

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederMultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat;

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederNat : Type;

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederNet : Type := _t300 (T ->? MultiSet P);

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaederP : Type;

76647324ed70f33b95a881b536d883daccf9568dChristian MaederSet : Type -> Type := \ S : Type . S ->? Unit;

d48085f765fca838c1d972d2123601997174583dChristian MaederSystem : Type := _t1007 Marking;

d48085f765fca838c1d972d2123601997174583dChristian MaederT : Type;

d48085f765fca838c1d972d2123601997174583dChristian Maeder_t1007 : +Type -> Type := _t1008 Net;

d48085f765fca838c1d972d2123601997174583dChristian Maeder_t1008 : +Type -> +Type -> Type < __*__;

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder_t1433 : +Type -> Type := _t1434 (T ->? T);

d48085f765fca838c1d972d2123601997174583dChristian Maeder_t1434 : +Type -> +Type -> Type := _t1435 (P ->? P);

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t1435 : +Type -> +Type -> +Type -> Type := _t1436 System;

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t1436 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__;

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t300 : +Type -> Type := _t301 (T ->? MultiSet P);

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder_t301 : +Type -> +Type -> Type := _t302 (Set P);

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t302 : +Type -> +Type -> +Type -> Type < __*__*__;

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t935 : +Type -> Type := _t936 (T ->? T);

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t936 : +Type -> +Type -> Type := _t937 (P ->? P);

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t937 : +Type -> +Type -> +Type -> Type := _t938 Net;

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder_t938 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedervars

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederElem : Type %(var_6)%;

76647324ed70f33b95a881b536d883daccf9568dChristian MaederS : Type %(var_62)%;

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederU : Type %(var_60)%;

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederV : Type %(var_63)%;

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedera : Type %(var_57)%

76647324ed70f33b95a881b536d883daccf9568dChristian Maederop 0 : Nat %(op)%

9a44a07ffc79da9852b6319bd6d9df81efe99809Christian Maederop 1 : Nat %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop False : Boolean %(constructor)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop MultiSetToSet : forall Elem : Type . MultiSet Elem -> Set Elem

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder %(op)%

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederop True : Boolean %(constructor)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop __*__ : forall S : Type; V : Type . Set S * Set V -> Set (S * V)

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder %(op)%

a39a820684c1974350f46593025e0bb279f41bc6Christian Maederop __+__ : Nat * Nat -> Nat %(op)%

a39a820684c1974350f46593025e0bb279f41bc6Christian Maederop __+__ : forall Elem : Type

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder . MultiSet Elem * MultiSet Elem -> MultiSet Elem

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __-__ : Nat * Nat -> Nat %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __-__ : forall Elem : Type

d48085f765fca838c1d972d2123601997174583dChristian Maeder . MultiSet Elem * MultiSet Elem -> MultiSet Elem

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder %(op)%

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederop __-__ : forall S : Type; V : Type . (S ->? V) * S -> S ->? V

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __::__-->__ : forall S : Type; V : Type

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder . Pred ((S ->? V) * Pred S * Pred V)

d48085f765fca838c1d972d2123601997174583dChristian Maeder %(op)%

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederop __::__-->__ : forall S : Type; V : Type

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __<=__ : Nat * Nat ->? Unit %(pred)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __<=__ : forall Elem : Type

d48085f765fca838c1d972d2123601997174583dChristian Maeder . Pred (MultiSet Elem * MultiSet Elem)

d48085f765fca838c1d972d2123601997174583dChristian Maeder %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __>__ : Nat * Nat ->? Unit %(pred)%

76647324ed70f33b95a881b536d883daccf9568dChristian Maederop __>=__ : Nat * Nat ->? Unit %(pred)%

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederop __[__/__] : forall S : Type; V : Type

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . (S ->? V) * S * V -> S ->? V

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder %(op)%

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

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

a39a820684c1974350f46593025e0bb279f41bc6Christian Maederop __disjointUnion__ : forall S : Type

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

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder %(op)%

d48085f765fca838c1d972d2123601997174583dChristian Maederop __intersection__ : forall Elem : Type

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder . MultiSet Elem * MultiSet Elem -> MultiSet Elem,

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder assoc, comm, idem %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop __intersection__ : forall S : Type . Set S * Set S -> Set S

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop __intersectionMap__ : forall S : Type; V : Type

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . (S ->? V) * (S ->? V) -> S ->? V

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder %(op)%

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

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop __isIn__ : forall Elem : Type . Pred (Elem * MultiSet Elem)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop __o__ : HomSys * HomSys ->? HomSys %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop __o__ : HomNet * HomNet ->? HomNet %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop __o__ : forall S : Type; V : Type; U : Type

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . (V ->? U) * (S ->? V) -> S ->? U

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder %(op)%

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop __restrict__ : forall S : Type; V : Type

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

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder %(op)%

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

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

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop __unionMap__ : forall S : Type; V : Type

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . (S ->? V) * (S ->? V) -> S ->? V

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder %(op)%

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

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maederop __||__ : forall S : Type; V : Type

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder . (S ->? V) * Set S -> S ->? V

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder %(op)%

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop cod : HomSys -> System %(op)%

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop cod : HomNet -> Net %(op)%

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederop dom : HomSys -> System %(op)%

3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederop dom : HomNet -> Net %(op)%

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

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop empty : Marking %(op)%

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

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop emptySet : forall S : Type . Set S %(op)%

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

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

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederop id : System ->? HomSys %(op)%

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maederop id : Net ->? HomNet %(op)%

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

98c47b3c137bdb20c53b6c1d346c0fb48b48d673Christian Maeder %(op)%

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

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

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

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

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

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop ker : forall S : Type; V : Type . (S ->? V) -> Pred (S * S)

a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop linMap : forall S : Type; V : Type

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder . (S ->? MultiSet V) -> MultiSet S ->? MultiSet V

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop marking : System -> Marking %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop min : Nat * Nat -> Nat %(op)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop net : System -> Net %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop places : Net -> Set P %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop placesMap : HomSys -> P ->? P %(op)%

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maederop placesMap : HomNet -> P ->? P %(op)%

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

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

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

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederop setToMultiSet : forall Elem : Type . Set Elem -> MultiSet Elem

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder %(op)%

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

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

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

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

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

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

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

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

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

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

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedervars

76647324ed70f33b95a881b536d883daccf9568dChristian MaederB : MultiSet Elem;

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederS : Set Elem;

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederh1 : HomSys;

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederh2 : HomSys

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederfree type Boolean ::= False | True %(ga_Boolean)%

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder. let S = MultiSetToSet B in

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder forall x : Elem

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder. def (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)

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

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

19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder (__o__ : (P ->? P) * (P ->? P) -> P ->? P)

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

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

19f104861f1832b452c9f98e59880d05e865d9bdChristian Maeder (__o__ : (T ->? T) * (T ->? T) -> T ->? T)

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

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

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (op cod : HomSys -> System) h2)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder as HomSys)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 7.7, is type variable 'S'

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

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

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder### Hint 31.6, is type variable 'Elem'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 31.6, rebound type variable 'Elem'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 33.10, not a kind 'MultiSet Elem'

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 35.17, not a class 'Elem'

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder### Hint 34.12, rebound variable 'S'

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder### Hint 34.12, rebound variable 'S'

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder### Hint 35.25-35.32, rejected 'Unit < Nat' of '((var x : Elem), (var S : Set Elem))'

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

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

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder '(x, S)'

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

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 37.7, rebound type variable 'S'

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 45.7, is type variable 'S'

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

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

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

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

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder### Hint 62.7, is type variable 'S'

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

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

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

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder### Hint 20.18-67.60, repeated declaration of '__intersection__' with type 'MultiSet Elem * MultiSet Elem -> MultiSet Elem'

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder### Hint 72.23, not a kind 'MultiSet P'

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

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder### Hint 72.37-72.51, rejected 'Unit < Nat' of '((var p1 : MultiSet P),

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (op range : forall S : Type; V : Type . (S ->? V) -> Set V)[T,

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder P ->? Nat]

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

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder### Hint 72.37-72.51, untypable term (with type: _v126_Elem * MultiSet _v126_Elem)

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder '(p1, range pre)'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 73.40-73.54, rejected 'Unit < Nat' of '((var p1 : MultiSet P),

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder (op range : forall S : Type; V : Type . (S ->? V) -> Set V)[T,

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder P ->? Nat]

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

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 73.40-73.54, untypable term (with type: _v217_Elem * MultiSet _v217_Elem)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder '(p1, range pre)'

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 81.19, not a class 'T'

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

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

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder typename 'P' (79.35)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder is not unifiable with type '_v319_V ->? Nat' (63.47)

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 80.8-80.35, untypable term (with type: (_v318_S ->? MultiSet _v319_V) * Set _v318_S * Set _v319_V)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder '(hp, places n1, places n2)'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 80.41-80.78, in type of '((var ht : T ->? T),

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

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

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder typename 'T' (79.45)

94b34b35075c9115a22b512fd4ec3fb290f13d59Christian Maeder is not unifiable with type '_v493_V ->? Nat' (63.47)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 80.41-80.78, untypable term (with type: (_v492_S ->? MultiSet _v493_V) * Set _v492_S * Set _v493_V)

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder '(ht, transitions n1, transitions n2)'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 81.24-81.43, rejected 'Unit < Nat' of '((var t : T), (op transitions : Net -> Set T) (var n1 : Net))'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder### Hint 81.24-81.43, untypable term (with type: _v670_Elem * MultiSet _v670_Elem)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder '(t, transitions n1)'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 95.38, not a class 'P'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 95.43-95.50, rejected 'Nat < Unit' of '((var x : P), (var m : Marking))'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder### Hint 95.43-95.50, untypable term (with type: _v969_S * Set _v969_S)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder '(x, m)'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder### Hint 95.55-95.62, rejected 'Unit < Nat' of '((var x : P), (var p : P ->? Unit))'

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder### Hint 95.55-95.62, untypable term (with type: _v990_Elem * MultiSet _v990_Elem)

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder '(x, p)'

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 104.19, not a class 'P'

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder### Hint 104.24-104.74, in type of '((op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)[P]

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ((var p : P),

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

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder (op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)[P]

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder ((var hp : P ->? P) (var p : P),

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

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder typename 'Nat' (28.38)

d48085f765fca838c1d972d2123601997174583dChristian Maeder is not unifiable with type '_v1208_Elem ->? Nat' (23.33)

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder

13f6b64b022fac1179149bfacf9a2ad908f7038dChristian Maeder### Hint 104.24-104.74, untypable term (with type: MultiSet _v1208_Elem * MultiSet _v1208_Elem)

13f6b64b022fac1179149bfacf9a2ad908f7038dChristian Maeder '(freq (p, marking sys1), freq (hp p, marking sys2))'

94b34b35075c9115a22b512fd4ec3fb290f13d59Christian Maeder### Hint 112.12, not a class 'HomSys'

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder### Hint 112.16, not a class 'HomSys'

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder### Hint 113.10-113.15, in type of '((var h2 : HomSys), (var h1 : HomSys))'

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder typename '_t1008' (93.8)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder is not unifiable with type '_t302 (Set P)' (71.34)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

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

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder '(h2, h1)'

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder### Hint 113.10-113.15, in type of '((var h2 : HomSys), (var h1 : HomSys))'

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder typename '__->?__' (54.17)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder is not unifiable with type '_t1435 (P ->? P)' (102.54)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder### Hint 113.10-113.15, untypable term (with type: (_v1446_V ->? _v1447_U) * (_v1448_S ->? _v1446_V))

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder '(h2, h1)'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 113.22-113.27, in type of '((var h2 : HomSys), (var h1 : HomSys))'

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder typename '_t1008' (93.8)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder is not unifiable with type '_t302 (Set P)' (71.34)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

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

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder '(h2, h1)'

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder### Hint 113.22-113.27, in type of '((var h2 : HomSys), (var h1 : HomSys))'

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder typename '__->?__' (54.17)

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder is not unifiable with type '_t1435 (P ->? P)' (102.54)

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder### Hint 113.22-113.27, untypable term (with type: (_v1938_V ->? _v1939_U) * (_v1940_S ->? _v1938_V))

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder '(h2, h1)'

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder### Hint 114.11, in type of '(var h1 : HomSys)'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder typename '_t1008' (93.8)

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder is not unifiable with type '_t302 (Set P)' (71.34)

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder

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

64b9ab8e743c8e284caab0ca522aa69b2e10ad15Christian Maeder 'h1'

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder### Hint 114.11, in type of '(var h1 : HomSys)'

64b9ab8e743c8e284caab0ca522aa69b2e10ad15Christian Maeder typename '__->?__' (47.15)

64b9ab8e743c8e284caab0ca522aa69b2e10ad15Christian Maeder is not unifiable with type '_t1435 (P ->? P)' (102.54)

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

64b9ab8e743c8e284caab0ca522aa69b2e10ad15Christian Maeder### Hint 114.11, untypable term (with type: _v2424_S ->? _v2425_V)

8c27ccd6d90c4dcdfbe52b95c1f0bef655918f26Christian Maeder 'h1'

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski### Hint 114.25, in type of '(var h2 : HomSys)'

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

is not unifiable with type '_t302 (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 '__->?__' (107.33)

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

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

'(placesMap h2, placesMap h1)'

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

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

is not unifiable with type '_t302 (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 '__->?__' (107.33)

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

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

'(placesMap h2, placesMap h1)'

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

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

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

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

'h1'

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

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

is not unifiable with type '_t302 (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 '__->?__' (108.38)

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

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

'(transitionsMap h2, transitionsMap h1)'

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

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

is not unifiable with type '_t302 (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 '__->?__' (108.38)

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

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

'(transitionsMap h2, transitionsMap h1)'

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

typename '_t1008' (93.8)

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

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

'h2'

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

typename '_t1008' (93.8)

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

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

'h1'

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

typename '_t1008' (93.8)

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

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

'h2'