PetriSystemCategory.hascasl.output revision b55cf4375478168316b212cbc7d261fb683645ff
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringop __+__, __-__, min : Nat * Nat -> Nat
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringpred __>=__, __<=__, __>__ : Nat * Nat
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poetteringfree type Boolean ::= True |
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poetteringvar S : Type; V : Type
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poetteringtype Set : Type -> Type := \ S : Type . S ->? Unit
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringop emptySet : Set S; {__} : S -> Set S;
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering __isIn__ : S * Set S ->? Unit;
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering __subset__ : Pred (Set (S) * Set (S));
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering __union__, __intersection__, __\\__ : Set S * Set S -> Set S;
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poettering __disjoint__ : Pred (Set (S) * Set (S));
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poettering __*__ : Set S * Set V -> Set (S * V);
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering __disjointUnion__ : Set S * Set S -> Set (S * Boolean);
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering injl, injr : S -> S * Boolean
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poetteringvar Elem : Type
a49408ec64063023524b964064d393c1fce36e4aKay Sieverstype MultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat
b925e72633bf98438f56a140520e07ec8c959e46Lennart Poetteringop __isIn__ : Pred (Elem * MultiSet Elem);
a0e155d440173ba524918cb3800350b452952082Lennart Poettering __<=__ : Pred (MultiSet Elem * MultiSet Elem); {} : MultiSet Elem;
e677657e8dddb33d1f1e32eda0ebc126e08a538dLennart Poettering {__} : Elem -> MultiSet Elem;
7d76f312889d54dcfe6fdde6eb055e890e7a615bLennart Poettering __+__, __-__, __intersection__ : MultiSet Elem * MultiSet Elem ->
7d76f312889d54dcfe6fdde6eb055e890e7a615bLennart Poettering MultiSet Elem;
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering freq : Elem * MultiSet Elem -> Nat;
18a5d7fffbcaea5ebd721df5f4938e8a347a2d3bLennart Poettering setToMultiSet : Set Elem -> MultiSet Elem
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poetteringvar Elem : Type
8e028bb1edf33da3ced2d353fbfafac7ad75e6beLennart Poetteringop MultiSetToSet : MultiSet Elem -> Set Elem
cca4aeeead1985f503d175eb1fcad9ed66f2e25dLennart Poetteringforall B : MultiSet Elem; S : Set Elem
cca4aeeead1985f503d175eb1fcad9ed66f2e25dLennart Poettering. let (var S : Set Elem) =
7ebdfc936e7c9697b9fa9441a502ad40abb7b245Lennart Poettering (op MultiSetToSet[Elem] :
7ebdfc936e7c9697b9fa9441a502ad40abb7b245Lennart Poettering forall Elem : Type . MultiSet Elem -> Set Elem)
7ebdfc936e7c9697b9fa9441a502ad40abb7b245Lennart Poettering (var B : MultiSet Elem)
16b879e3eeb25f7b0d517682a4e8b62f39c149f2Kay Sievers in forall x : Elem
16b879e3eeb25f7b0d517682a4e8b62f39c149f2Kay Sievers ((op __isIn__[Elem] : forall S : Type . S * Set S ->? Unit)
16b879e3eeb25f7b0d517682a4e8b62f39c149f2Kay Sievers ((var x : Elem), (var S : Set Elem)),
16b879e3eeb25f7b0d517682a4e8b62f39c149f2Kay Sievers (pred __>__ : Nat * Nat)
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering ((op freq[Elem] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
9408a2d295a312a5472345090e28e0502570494bLennart Poettering ((var x : Elem), (var B : MultiSet Elem)),
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering (op 0 : Nat)))
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sieverstype MapMultiSet : Type -> Type := \ S : Type . MultiSet S ->?
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sieversop sumN : (Nat ->? Nat) -> Nat -> Nat; sumSet : Set Nat ->? Nat;
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poettering sum : (a ->? Nat) -> Pred a ->? Nat
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poetteringvar S : Type; V : Type; U : Type
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sieverstype Map : Type -> Type := \ S : Type . S ->? S
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sieversop dom : (S ->? V) -> Set S; range : (S ->? V) -> Set V;
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sievers image : (S ->? V) -> Set S -> Set V; emptyMap : (S ->? V);
7a03b1970c35c2b0924152404fb7526965eb4f3cKay Sievers __::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sievers __[__/__] : (S ->? V) * S * V -> (S ->? V);
7a03b1970c35c2b0924152404fb7526965eb4f3cKay Sievers __-__ : (S ->? V) * S -> (S ->? V);
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering __o__ : (V ->? U) * (S ->? V) -> (S ->? U);
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering __||__ : (S ->? V) * Set S -> (S ->? V); undef__ : S ->? V;
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering ker : (S ->? V) -> Pred (S * S); injective : Pred (S ->? V);
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering __intersectionMap__, __unionMap__ : (S ->? V) * (S ->? V) ->
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering __restrict__ : (S ->? V) * Set S -> (S ->? V)
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sieversvar S : Type; V : Type
a49408ec64063023524b964064d393c1fce36e4aKay Sieversop __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers freeMap : Map S -> MapMultiSet S;
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poetteringop __intersection__ : MultiSet Elem * MultiSet Elem ->
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers MultiSet Elem, assoc, comm, idem
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieverstype Net = {(p, pre, post) : Set P * (T ->? MultiSet P) *
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers (T ->? MultiSet P) . __/\__
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers ((op dom[T; P ->? Nat] :
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers forall S : Type; V : Type .
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers (S ->? V) -> Set S)
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers (var pre : T ->? MultiSet P),
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers (op dom[T; P ->? Nat] :
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sievers forall S : Type; V : Type .
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poettering (S ->? V) -> Set S)
a49408ec64063023524b964064d393c1fce36e4aKay Sievers (var post : T ->? MultiSet P)),
a49408ec64063023524b964064d393c1fce36e4aKay Sievers forall p1 : MultiSet P
a49408ec64063023524b964064d393c1fce36e4aKay Sievers ((op __isIn__[P ->? Nat] :
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering forall S : Type . S * Set S ->? Unit)
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering ((var p1 : MultiSet P),
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering (op range[T; P ->? Nat] :
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering forall S : Type; V : Type .
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering (S ->? V) -> Set V)
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering (var pre : T ->? MultiSet P)),
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering (op __subset__[P] :
7fc7012b8b54bdd6610d32649d4ee9c938a4843dLennart Poettering forall S : Type . Pred (Set S * Set S))
430c18ed7f576fd9041b0a02e7c4210bdd020a25Lennart Poettering ((op MultiSetToSet[P] :
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering forall Elem : Type .
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering MultiSet Elem -> Set Elem)
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering (var p1 : MultiSet P),
a49408ec64063023524b964064d393c1fce36e4aKay Sievers (var p : Set P)))),
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering forall p1 : MultiSet P
a49408ec64063023524b964064d393c1fce36e4aKay Sievers ((op __isIn__[P ->? Nat] :
a49408ec64063023524b964064d393c1fce36e4aKay Sievers forall S : Type . S * Set S ->? Unit)
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering ((var p1 : MultiSet P),
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering (op range[T; P ->? Nat] :
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering forall S : Type; V : Type .
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poettering (S ->? V) -> Set V)
a49408ec64063023524b964064d393c1fce36e4aKay Sievers (var pre : T ->? MultiSet P)),
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poettering (op __subset__[P] :
b5c6cf87342bedeb67fbbc4f3f512af1603a461cLennart Poettering forall S : Type . Pred (Set S * Set S))
b5c6cf87342bedeb67fbbc4f3f512af1603a461cLennart Poettering ((op MultiSetToSet[P] :
3185a36b05d53757a412f847d8c510978b9b00f0Lennart Poettering forall Elem : Type .
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers MultiSet Elem -> Set Elem)
3185a36b05d53757a412f847d8c510978b9b00f0Lennart Poettering (var p1 : MultiSet P),
b8bb3e8f346468e61dcc7a6aba5e7ac9c623d964Lennart Poettering (var p : Set P))))}
b8bb3e8f346468e61dcc7a6aba5e7ac9c623d964Lennart Poetteringop places : Net -> Set P; transitions : Net -> Set T;
f959c5e63a9080cbff42ac4160154f8a6b508e7aLennart Poettering preMap, postMap : Net -> (T ->? MultiSet P)
f959c5e63a9080cbff42ac4160154f8a6b508e7aLennart Poetteringtype HomNet = {(n1, hp, ht, n2) : Net * (P ->? P) * (T ->? T) *
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poettering ((op __::__-->__[P; P] :
47ae6e6760301ecae086e984b0b23f2db9663b28Lennart Poettering forall S : Type; V : Type .
47ae6e6760301ecae086e984b0b23f2db9663b28Lennart Poettering Pred ((S ->? V) * Pred S * Pred V))
487a15bb726698f84503682ccbc30375586c52deLennart Poettering ((var hp : P ->? P),
487a15bb726698f84503682ccbc30375586c52deLennart Poettering (op places : Net -> Set P) (var n1 : Net),
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering (op places : Net -> Set P) (var n2 : Net)),
2c4b304e64ca674e1a79a7e5c83a996a03611a17Lennart Poettering (op __::__-->__[T; T] :