PetriSystemCategory.hascasl.output revision a6f84880cea4485fba85b521d122eba73b0df70b
type Nat
ops 0, 1 : Nat
ops __+__, __-__, min : Nat * Nat -> Nat
preds __>=__, __<=__, __>__ : Nat * Nat
free type Boolean ::= True | False
vars S, V : Type
type Set S := S ->? Unit
ops emptySet : Set S;
{__} : S -> Set S;
__isIn__ : S * Set S ->? Unit;
__subset__ : Pred (Set (S) * Set (S));
__union__, __intersection__, __\\__ : Set S * Set S -> Set S;
__disjoint__ : Pred (Set (S) * Set (S));
__*__ : Set S * Set V -> Set (S * V);
__disjointUnion__ : Set S * Set S -> Set (S * Boolean);
injl, injr : S -> S * Boolean
var Elem : Type
type MultiSet Elem := Elem ->? Nat
ops __isIn__ : Pred (Elem * MultiSet Elem);
__<=__ : Pred (MultiSet Elem * MultiSet Elem);
{} : MultiSet Elem;
{__} : Elem -> MultiSet Elem;
__+__, __-__, __intersection__
: MultiSet Elem * MultiSet Elem -> MultiSet Elem;
freq : Elem * MultiSet Elem -> Nat;
setToMultiSet : Set Elem -> MultiSet Elem
var Elem : Type
op MultiSetToSet : MultiSet Elem -> Set Elem
forall B : MultiSet Elem; S : Set Elem
. let S = MultiSetToSet B in
forall x : Elem . x isIn S <=> freq (x, B) > 0;
var S : Type
type MapMultiSet S := MultiSet S ->? MultiSet S
var a : Type
ops sumN : (Nat ->? Nat) -> Nat -> Nat;
sumSet : Set Nat ->? Nat;
sum : (a ->? Nat) -> Pred a ->? Nat
vars S, V, U : Type
type Map S := S ->? S
ops dom : (S ->? V) -> Set S;
range : (S ->? V) -> Set V;
image : (S ->? V) -> Set S -> Set V;
emptyMap : (S ->? V);
__::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));
__[__/__] : (S ->? V) * S * V -> (S ->? V);
__-__ : (S ->? V) * S -> (S ->? V);
__o__ : (V ->? U) * (S ->? V) -> (S ->? U);
__||__ : (S ->? V) * Set S -> (S ->? V);
undef__ : S ->? V;
ker : (S ->? V) -> Pred (S * S);
injective : Pred (S ->? V);
__intersectionMap__, __unionMap__
: (S ->? V) * (S ->? V) -> (S ->? V);
__restrict__ : (S ->? V) * Set S -> (S ->? V)
vars S, V : Type
ops __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);
freeMap : Map S -> MapMultiSet S;
linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)
op __intersection__
: MultiSet Elem * MultiSet Elem -> MultiSet Elem, assoc, comm, idem
types P, T
type Net =
{(p, pre, post) : Set P * (T ->? MultiSet P) * (T ->? MultiSet P)
. (dom pre = dom post
/\ forall p1 : MultiSet P
. p1 isIn range pre => MultiSetToSet p1 subset p)
/\ forall p1 : MultiSet P
. p1 isIn range pre => MultiSetToSet p1 subset p
}
ops places : Net -> Set P;
transitions : Net -> Set T;
preMap, postMap : Net -> (T ->? MultiSet P)
type HomNet =
{(n1, hp, ht, n2) : Net * (P ->? P) * (T ->? T) * Net
. hp :: places n1 --> places n2
/\ ht :: transitions n1 --> transitions n2
/\ forall t : T
. t isIn transitions n1
=> freeMap hp (preMap n1 t) = preMap n2 (ht t)
/\ freeMap hp (postMap n1 t) = postMap n2 (ht t)
}
ops dom : HomNet -> Net;
cod : HomNet -> Net;
placesMap : HomNet -> (P ->? P);
transitionsMap : HomNet -> (T ->? T);
id : Net ->? HomNet;
__o__ : HomNet * HomNet ->? HomNet
pred injective : HomNet
type Marking := MultiSet P
type System =
{(n, m) : Net * Marking
. let (p, pre1, post1) = n in forall x : P . x isIn m => x isIn p
}
ops marking : System -> Marking;
net : System -> Net;
empty : Marking;
__|<__> : System * T -> System;
__|<__> : System * MultiSet T ->? System
type HomSys =
{(sys1, hp, ht, sys2) : System * (P ->? P) * (T ->? T) * System
. ((net sys1, hp, ht, net sys2) in HomNet)
/\ forall p : P
. freq (p, marking sys1) <= freq (hp p, marking sys2)
}
ops dom : HomSys -> System;
cod : HomSys -> System;
placesMap : HomSys -> (P ->? P);
transitionsMap : HomSys -> (T ->? T);
id : System ->? HomSys;
__o__ : HomSys * HomSys ->? HomSys
pred injective : HomSys
forall h1, h2 : HomSys
. def (h2 o h1)
=> h2 o h1
= ((dom h1, placesMap h2 o placesMap h1,
transitionsMap h2 o transitionsMap h1, cod h2)
as HomSys);
types
Boolean : Type;
HomNet : Type;
HomSys : Type;
Map : Type -> Type;
MapMultiSet : Type -> Type;
Marking : Type;
MultiSet : Type -> Type;
Nat : Type;
Net : Type;
P : Type;
Set : Type -> Type;
System : Type;
T : Type;
gn_t100[gn_t99[gn_t98[gn_t97[HomNet]]]] : +Type ->
+Type -> +Type -> +Type -> Type;
gn_t121[System] : +Type -> Type;
gn_t122[gn_t121[System]] : +Type -> +Type -> Type;
gn_t164[HomSys] : +Type -> Type;
gn_t165[gn_t164[HomSys]] : +Type -> +Type -> Type;
gn_t166[gn_t165[gn_t164[HomSys]]] : +Type ->
+Type -> +Type -> Type;
gn_t167[gn_t166[gn_t165[gn_t164[HomSys]]]] : +Type ->
+Type -> +Type -> +Type -> Type;
gn_t74[Net] : +Type -> Type;
gn_t75[gn_t74[Net]] : +Type -> +Type -> Type;
gn_t76[gn_t75[gn_t74[Net]]] : +Type -> +Type -> +Type -> Type;
gn_t97[HomNet] : +Type -> Type;
gn_t98[gn_t97[HomNet]] : +Type -> +Type -> Type;
gn_t99[gn_t98[gn_t97[HomNet]]] : +Type -> +Type -> +Type -> Type
types
gn_t100[gn_t99[gn_t98[gn_t97[HomNet]]]] < __*__*__*__;
gn_t122[gn_t121[System]] < __*__;
gn_t167[gn_t166[gn_t165[gn_t164[HomSys]]]] < __*__*__*__;
gn_t76[gn_t75[gn_t74[Net]]] < __*__*__
types
HomNet := gn_t97[HomNet] Net;
HomSys := gn_t164[HomSys] System;
Map (S : Type) := S ->? S;
MapMultiSet (S : Type) := MultiSet S ->? MultiSet S;
Marking := MultiSet P;
MultiSet (Elem : Type) := Elem ->? Nat;
Net := gn_t74[Net] (T ->? MultiSet P);
Set (S : Type) := S ->? Unit;
System := gn_t121[System] Marking;
gn_t121[System] := gn_t122[gn_t121[System]] Net;
gn_t164[HomSys] := gn_t165[gn_t164[HomSys]] (T ->? T);
gn_t165[gn_t164[HomSys]]
:= gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P);
gn_t166[gn_t165[gn_t164[HomSys]]]
:= gn_t167[gn_t166[gn_t165[gn_t164[HomSys]]]] System;
gn_t74[Net] := gn_t75[gn_t74[Net]] (T ->? MultiSet P);
gn_t75[gn_t74[Net]] := gn_t76[gn_t75[gn_t74[Net]]] (Set P);
gn_t97[HomNet] := gn_t98[gn_t97[HomNet]] (T ->? T);
gn_t98[gn_t97[HomNet]] := gn_t99[gn_t98[gn_t97[HomNet]]] (P ->? P);
gn_t99[gn_t98[gn_t97[HomNet]]]
:= gn_t100[gn_t99[gn_t98[gn_t97[HomNet]]]] Net
vars
Elem : Type %(var_6)%;
S : Type %(var_18)%;
U : Type %(var_16)%;
V : Type %(var_19)%;
a : Type %(var_13)%
op 0 : Nat %(op)%
op 1 : Nat %(op)%
op False : Boolean %(constructor)%
op MultiSetToSet : forall Elem : Type . MultiSet Elem -> Set Elem
%(op)%
op True : Boolean %(constructor)%
op __*__ : forall S : Type; V : Type . Set S * Set V -> Set (S * V)
%(op)%
op __+__ : Nat * Nat -> Nat %(op)%
op __+__ : forall Elem : Type
. MultiSet Elem * MultiSet Elem -> MultiSet Elem
%(op)%
op __-__ : Nat * Nat -> Nat %(op)%
op __-__ : forall Elem : Type
. MultiSet Elem * MultiSet Elem -> MultiSet Elem
%(op)%
op __-__ : forall S : Type; V : Type . (S ->? V) * S -> S ->? V
%(op)%
op __::__-->__ : forall S : Type; V : Type
. Pred ((S ->? V) * Pred S * Pred V)
%(op)%
op __::__-->__ : forall S : Type; V : Type
. Pred ((S ->? MultiSet V) * Set S * Set V)
%(op)%
op __<=__ : Nat * Nat ->? Unit %(pred)%
op __<=__ : forall Elem : Type
. Pred (MultiSet Elem * MultiSet Elem)
%(op)%
op __>__ : Nat * Nat ->? Unit %(pred)%
op __>=__ : Nat * Nat ->? Unit %(pred)%
op __[__/__] : forall S : Type; V : Type
. (S ->? V) * S * V -> S ->? V
%(op)%
op __\\__ : forall S : Type . Set S * Set S -> Set S %(op)%
op __disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%
op __disjointUnion__ : forall S : Type
. Set S * Set S -> Set (S * Boolean)
%(op)%
op __intersection__ : forall Elem : Type
. MultiSet Elem * MultiSet Elem -> MultiSet Elem
%(op)%
op __intersection__ : forall S : Type . Set S * Set S -> Set S
%(op)%
op __intersectionMap__ : forall S : Type; V : Type
. (S ->? V) * (S ->? V) -> S ->? V
%(op)%
op __isIn__ : forall S : Type . S * Set S ->? Unit %(op)%
op __isIn__ : forall Elem : Type . Pred (Elem * MultiSet Elem)
%(op)%
op __o__ : HomNet * HomNet ->? HomNet %(op)%
op __o__ : HomSys * HomSys ->? HomSys %(op)%
op __o__ : forall S : Type; V : Type; U : Type
. (V ->? U) * (S ->? V) -> S ->? U
%(op)%
op __restrict__ : forall S : Type; V : Type
. (S ->? V) * Set S -> S ->? V
%(op)%
op __subset__ : forall S : Type . Pred (Set S * Set S) %(op)%
op __union__ : forall S : Type . Set S * Set S -> Set S %(op)%
op __unionMap__ : forall S : Type; V : Type
. (S ->? V) * (S ->? V) -> S ->? V
%(op)%
op __|<__> : System * T -> System %(op)%
op __|<__> : System * MultiSet T ->? System %(op)%
op __||__ : forall S : Type; V : Type
. (S ->? V) * Set S -> S ->? V
%(op)%
op cod : HomNet -> Net %(op)%
op cod : HomSys -> System %(op)%
op dom : HomNet -> Net %(op)%
op dom : HomSys -> System %(op)%
op dom : forall S : Type; V : Type . (S ->? V) -> Set S %(op)%
op empty : Marking %(op)%
op emptyMap : forall S : Type; V : Type . S ->? V %(op)%
op emptySet : forall S : Type . Set S %(op)%
op freeMap : forall S : Type . Map S -> MapMultiSet S %(op)%
op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat %(op)%
op id : System ->? HomSys %(op)%
op id : Net ->? HomNet %(op)%
op image : forall S : Type; V : Type . (S ->? V) -> Set S -> Set V
%(op)%
op injective : HomNet ->? Unit %(pred)%
op injective : HomSys ->? Unit %(pred)%
op injective : forall S : Type; V : Type . Pred (S ->? V) %(op)%
op injl : forall S : Type . S -> S * Boolean %(op)%
op injr : forall S : Type . S -> S * Boolean %(op)%
op ker : forall S : Type; V : Type . (S ->? V) -> Pred (S * S)
%(op)%
op linMap : forall S : Type; V : Type
. (S ->? MultiSet V) -> MultiSet S ->? MultiSet V
%(op)%
op marking : System -> Marking %(op)%
op min : Nat * Nat -> Nat %(op)%
op net : System -> Net %(op)%
op places : Net -> Set P %(op)%
op placesMap : HomNet -> P ->? P %(op)%
op placesMap : HomSys -> P ->? P %(op)%
op postMap : Net -> T ->? MultiSet P %(op)%
op preMap : Net -> T ->? MultiSet P %(op)%
op range : forall S : Type; V : Type . (S ->? V) -> Set V %(op)%
op setToMultiSet : forall Elem : Type . Set Elem -> MultiSet Elem
%(op)%
op sum : forall a : Type . (a ->? Nat) -> Pred a ->? Nat %(op)%
op sumN : (Nat ->? Nat) -> Nat -> Nat %(op)%
op sumSet : Set Nat ->? Nat %(op)%
op transitions : Net -> Set T %(op)%
op transitionsMap : HomNet -> T ->? T %(op)%
op transitionsMap : HomSys -> T ->? T %(op)%
op undef__ : forall S : Type; V : Type . S ->? V %(op)%
op {__} : forall Elem : Type . Elem -> MultiSet Elem %(op)%
op {__} : forall S : Type . S -> Set S %(op)%
op {} : forall Elem : Type . MultiSet Elem %(op)%
free type Boolean ::= False | True %(ga_Boolean)%
forall Elem : Type; B : MultiSet Elem
. let S = MultiSetToSet B in
forall x : Elem
. (op __isIn__ : forall S : Type . S * Set S ->? Unit) (x, S)
<=> freq (x, B) > 0
forall p : Set P; pre : T ->? MultiSet P; post : T ->? MultiSet P
. ((p, pre, post) in Net)
<=> ((op dom : forall S : Type; V : Type . (S ->? V) -> Set S) pre
= (op dom : forall S : Type; V : Type . (S ->? V) -> Set S) post
/\ forall p1 : MultiSet P
. (op __isIn__ : forall S : Type . S * Set S ->? Unit)
(p1, range pre)
=> MultiSetToSet p1 subset p)
/\ forall p1 : MultiSet P
. (op __isIn__ : forall S : Type . S * Set S ->? Unit)
(p1, range pre)
=> MultiSetToSet p1 subset p
forall n1 : Net; hp : P ->? P; ht : T ->? T; n2 : Net
. ((n1, hp, ht, n2) in HomNet)
<=> (op __::__-->__ :
forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))
(hp, places n1, places n2)
/\ (op __::__-->__ :
forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))
(ht, transitions n1, transitions n2)
/\ forall t : T
. (op __isIn__ : forall S : Type . S * Set S ->? Unit)
(t, transitions n1)
=> freeMap hp (preMap n1 t) = preMap n2 (ht t)
/\ freeMap hp (postMap n1 t) = postMap n2 (ht t)
forall n : Net; m : Marking
. ((n, m) in System)
<=> let (p, pre1, post1) = n in
forall x : P
. (op __isIn__ : forall Elem : Type . Pred (Elem * MultiSet Elem))
(x, m)
=> (op __isIn__ : forall S : Type . S * Set S ->? Unit) (x, p)
forall sys1 : System; hp : P ->? P; ht : T ->? T; sys2 : System
. ((sys1, hp, ht, sys2) in HomSys)
<=> ((net sys1, hp, ht, net sys2) in HomNet)
/\ forall p : P
. (pred __<=__ : Nat * Nat)
(freq (p, marking sys1), freq (hp p, marking sys2))
forall h1 : HomSys; h2 : HomSys
. def (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)
=> (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)
= (((op dom : HomSys -> System) h1,
(op __o__ :
forall S : Type; V : Type; U : Type
. (V ->? U) * (S ->? V) -> S ->? U)
((op placesMap : HomSys -> P ->? P) h2,
(op placesMap : HomSys -> P ->? P) h1),
(op __o__ :
forall S : Type; V : Type; U : Type
. (V ->? U) * (S ->? V) -> S ->? U)
((op transitionsMap : HomSys -> T ->? T) h2,
(op transitionsMap : HomSys -> T ->? T) h1),
(op cod : HomSys -> System) h2)
as HomSys)
### Hint 3.28,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 3.28,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 3.28,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 3.28,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 3.28,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 3.28,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cpo}
found: {Type}
### Hint 4.34,
no kind found for 'Nat'
expected: {Cppo}
found: {Type}
### Hint 7.7, is type variable 'S'
### Hint 7.9, is type variable 'V'
### Hint 11.18,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 11.18,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 12.25-12.29,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 12.25-12.29,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 13.46-13.50,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 14.28-14.32,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 14.28-14.32,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 15.15-15.19,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 15.15-15.19,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 15.37,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 15.37,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 16.28-16.32,
no kind found for 'Set S'
expected: {Cpo}
found: {Type}
### Hint 16.28-16.32,
no kind found for 'Set S'
expected: {Cppo}
found: {Type}
### Hint 16.50,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 16.50,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 17.24,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 17.24,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 17.24,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 17.24,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 19.7-19.10, is type variable 'Elem'
### Hint 22.25,
no kind found for 'Elem'
expected: {Cpo}
found: {Type}
### Hint 22.25,
no kind found for 'Elem'
expected: {Cppo}
found: {Type}
### Hint 23.24-23.33,
no kind found for 'MultiSet Elem'
expected: {Cpo}
found: {Type}
### Hint 23.24-23.33,
no kind found for 'MultiSet Elem'
expected: {Cppo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cpo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cppo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cpo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cppo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cpo}
found: {Type}
### Hint 27.21-27.30,
no kind found for 'MultiSet Elem'
expected: {Cppo}
found: {Type}
### Hint 28.14,
no kind found for 'Elem'
expected: {Cpo}
found: {Type}
### Hint 28.14,
no kind found for 'Elem'
expected: {Cppo}
found: {Type}
### Hint 31.6-31.9, is type variable 'Elem'
### Hint 31.6-31.9, rebound type variable 'Elem'
### Hint 33.10, not a kind 'MultiSet Elem'
### Hint 33.27, not a kind 'Set Elem'
### Warning 33.26, variable also known as type variable 'S'
### Hint 35.17, not a class 'Elem'
### Hint 34.12, rebound variable 'S'
### Warning 34.12, variable also known as type variable 'S'
### Hint 34.12, rebound variable 'S'
### Warning 34.12, variable also known as type variable 'S'
### Hint 35.25-35.32,
rejected 'Unit < Nat' of '((var x : Elem), (var S : Set Elem))'
### Hint 35.25-35.32,
untypeable term (with type: _v9_Elem * MultiSet _v9_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 51.33-51.37,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 51.33-51.37,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 52.21-52.25,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 52.21-52.25,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 53.18-53.22,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 53.18-53.22,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 54.16-54.20,
no kind found for 'V ->? U'
expected: {Cpo}
found: {Type}
### Hint 54.16-54.20,
no kind found for 'V ->? U'
expected: {Cppo}
found: {Type}
### Hint 55.17-55.21,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 55.17-55.21,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 57.30,
no kind found for 'S'
expected: {Cpo}
found: {Type}
### Hint 57.30,
no kind found for 'S'
expected: {Cppo}
found: {Type}
### Hint 59.44-59.48,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 59.44-59.48,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 59.44-59.48,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 59.44-59.48,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### Hint 60.23-60.27,
no kind found for 'S ->? V'
expected: {Cpo}
found: {Type}
### Hint 60.23-60.27,
no kind found for 'S ->? V'
expected: {Cppo}
found: {Type}
### 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 63.33-63.47,
no kind found for 'S ->? MultiSet V'
expected: {Cpo}
found: {Type}
### Hint 63.33-63.47,
no kind found for 'S ->? MultiSet V'
expected: {Cppo}
found: {Type}
### Hint 67.27-67.36,
no kind found for 'MultiSet Elem'
expected: {Cpo}
found: {Type}
### Hint 67.27-67.36,
no kind found for 'MultiSet Elem'
expected: {Cppo}
found: {Type}
### Hint 20.18-67.60,
repeated declaration of '__intersection__' with type
'MultiSet Elem * MultiSet Elem -> MultiSet Elem'
### Hint 71.30-71.34,
no kind found for 'Set P'
expected: {Cpo}
found: {Type}
### Hint 71.30-71.34,
no kind found for 'Set P'
expected: {Cppo}
found: {Type}
### Hint 72.23, not a kind 'MultiSet P'
### Hint 73.26, not a kind 'MultiSet P'
### Hint 72.37-72.51,
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,
untypeable term (with type: _v35_Elem * MultiSet _v35_Elem)
'(p1, range pre)'
### Hint 73.40-73.54,
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,
untypeable term (with type: _v55_Elem * MultiSet _v55_Elem)
'(p1, range pre)'
### Hint 79.23,
no kind found for 'Net'
expected: {Cpo}
found: {Type}
### Hint 79.23,
no kind found for 'Net'
expected: {Cppo}
found: {Type}
### Hint 81.19, not a class 'T'
### Hint 80.8-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 '_v80_V ->? Nat' (63.47)
### Hint 80.8-80.35,
untypeable term (with type: (_v79_S ->? MultiSet _v80_V) * Set _v79_S * Set _v80_V)
'(hp, places n1, places n2)'
### Hint 80.41-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 '_v84_V ->? Nat' (63.47)
### Hint 80.41-80.78,
untypeable term (with type: (_v83_S ->? MultiSet _v84_V) * Set _v83_S * Set _v84_V)
'(ht, transitions n1, transitions n2)'
### Hint 81.24-81.43,
rejected 'Unit < Nat' of '((var t : T), (op transitions : Net -> Set T) (var n1 : Net))'
### Hint 81.24-81.43,
untypeable term (with type: _v86_Elem * MultiSet _v86_Elem)
'(t, transitions n1)'
### Hint 89.15,
no kind found for 'HomNet'
expected: {Cpo}
found: {Type}
### Hint 89.15,
no kind found for 'HomNet'
expected: {Cppo}
found: {Type}
### Hint 93.26,
no kind found for 'Net'
expected: {Cpo}
found: {Type}
### Hint 93.26,
no kind found for 'Net'
expected: {Cppo}
found: {Type}
### Hint 95.38, not a class 'P'
### Hint 95.43-95.50,
rejected 'Nat < Unit' of '((var x : P), (var m : Marking))'
### Hint 95.43-95.50,
untypeable term (with type: _v117_S * Set _v117_S) '(x, m)'
### Hint 95.55-95.62,
rejected 'Unit < Nat' of '((var x : P), (var p : P ->? Unit))'
### Hint 95.55-95.62,
untypeable term (with type: _v120_Elem * MultiSet _v120_Elem)
'(x, p)'
### Hint 99.20,
no kind found for 'System'
expected: {Cpo}
found: {Type}
### Hint 99.20,
no kind found for 'System'
expected: {Cppo}
found: {Type}
### Hint 100.20,
no kind found for 'System'
expected: {Cpo}
found: {Type}
### Hint 100.20,
no kind found for 'System'
expected: {Cppo}
found: {Type}
### Hint 102.39,
no kind found for 'System'
expected: {Cpo}
found: {Type}
### Hint 102.39,
no kind found for 'System'
expected: {Cppo}
found: {Type}
### Hint 104.19, not a class 'P'
### Hint 104.24-104.69,
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 '_v159_Elem ->? Nat' (23.33)
### Hint 104.24-104.69,
untypeable term (with type: MultiSet _v159_Elem * MultiSet _v159_Elem)
'(freq (p, marking sys1), freq (hp p, marking sys2))'
### Hint 110.16,
no kind found for 'HomSys'
expected: {Cpo}
found: {Type}
### Hint 110.16,
no kind found for 'HomSys'
expected: {Cppo}
found: {Type}
### Hint 112.12, not a class 'HomSys'
### Hint 112.16, not a class 'HomSys'
### Hint 113.10,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 113.10-113.15,
untypeable term (with type: HomNet * HomNet) '(h2, h1)'
### Hint 113.10-113.15,
in type of '((var h2 : HomSys), (var h1 : HomSys))'
typename '__->?__' (54.17)
is not unifiable with type 'gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P)' (102.54)
### Hint 113.10-113.15,
untypeable term (with type: (_v169_V ->? _v170_U) * (_v171_S ->? _v169_V))
'(h2, h1)'
### Hint 113.22,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 113.22-113.27,
untypeable term (with type: HomNet * HomNet) '(h2, h1)'
### Hint 113.22-113.27,
in type of '((var h2 : HomSys), (var h1 : HomSys))'
typename '__->?__' (54.17)
is not unifiable with type 'gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P)' (102.54)
### Hint 113.22-113.27,
untypeable term (with type: (_v216_V ->? _v217_U) * (_v218_S ->? _v216_V))
'(h2, h1)'
### Hint 114.11,
in type of '(var h1 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.11, untypeable term (with type: HomNet) 'h1'
### Hint 114.11,
in type of '(var h1 : HomSys)'
typename '__->?__' (47.15)
is not unifiable with type 'gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P)' (102.54)
### Hint 114.11,
untypeable term (with type: _v220_S ->? _v221_V) 'h1'
### Hint 114.25,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.25, untypeable term (with type: HomNet) 'h2'
### Hint 114.15-114.25,
in type of '(op placesMap : HomSys -> P ->? P) (var h2 : HomSys)'
typename '__->?__' (107.33)
is not unifiable with type 'gn_t99[gn_t98[gn_t97[HomNet]]] (P ->? P)' (79.35)
### Hint 114.15-114.40,
untypeable term (with type: HomNet * HomNet)
'(placesMap h2, placesMap h1)'
### Hint 114.25,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.25, untypeable term (with type: HomNet) 'h2'
### Hint 114.15-114.25,
in type of '(op placesMap : HomSys -> P ->? P) (var h2 : HomSys)'
typename '__->?__' (107.33)
is not unifiable with type 'gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P)' (102.54)
### Hint 114.15-114.40,
untypeable term (with type: HomSys * HomSys)
'(placesMap h2, placesMap h1)'
### Hint 114.25,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.25, untypeable term (with type: HomNet) 'h2'
### Hint 114.40,
in type of '(var h1 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.40, untypeable term (with type: HomNet) 'h1'
### Hint 114.59,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.59, untypeable term (with type: HomNet) 'h2'
### Hint 114.44-114.59,
in type of '(op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys)'
typename '__->?__' (108.38)
is not unifiable with type 'gn_t99[gn_t98[gn_t97[HomNet]]] (P ->? P)' (79.35)
### Hint 114.44-114.79,
untypeable term (with type: HomNet * HomNet)
'(transitionsMap h2, transitionsMap h1)'
### Hint 114.59,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.59, untypeable term (with type: HomNet) 'h2'
### Hint 114.44-114.59,
in type of '(op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys)'
typename '__->?__' (108.38)
is not unifiable with type 'gn_t166[gn_t165[gn_t164[HomSys]]] (P ->? P)' (102.54)
### Hint 114.44-114.79,
untypeable term (with type: HomSys * HomSys)
'(transitionsMap h2, transitionsMap h1)'
### Hint 114.59,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.59, untypeable term (with type: HomNet) 'h2'
### Hint 114.79,
in type of '(var h1 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.79, untypeable term (with type: HomNet) 'h1'
### Hint 114.86,
in type of '(var h2 : HomSys)'
typename 'gn_t122[gn_t121[System]]' (93.8)
is not unifiable with type 'gn_t76[gn_t75[gn_t74[Net]]] (Set P)' (71.34)
### Hint 114.86, untypeable term (with type: HomNet) 'h2'