8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovatype Nat

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaop 0, 1 : Nat

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaop __+__, __-__, min : Nat * Nat -> Nat

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovapred __>=__, __<=__, __>__ : Nat * Nat

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakovafree type Boolean ::= True |

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova False

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakovavar S : Type; V : Type

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakovatype Set : Type -> Type := \ S : Type . S ->? Unit

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakovaop emptySet : Set S;

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova {__} : S -> Set S;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova __isIn__ : S * Set S ->? Unit;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova __subset__ : Pred (Set (S) * Set (S));

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __union__, __intersection__, __\\__ : Set S * Set S -> Set S;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __disjoint__ : Pred (Set (S) * Set (S));

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __*__ : Set S * Set V -> Set (S * V);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __disjointUnion__ : Set S * Set S -> Set (S * Boolean);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova injl, injr : S -> S * Boolean

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovavar Elem : Type

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatype MultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaop __isIn__ : Pred (Elem * MultiSet Elem);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __<=__ : Pred (MultiSet Elem * MultiSet Elem);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova {} : MultiSet Elem;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova {__} : Elem -> MultiSet Elem;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova __+__, __-__, __intersection__ : MultiSet Elem * MultiSet Elem ->

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova MultiSet Elem;

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova freq : Elem * MultiSet Elem -> Nat;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova setToMultiSet : Set Elem -> MultiSet Elem

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavar Elem : Type

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaop MultiSetToSet : MultiSet Elem -> Set Elem

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaforall B : MultiSet Elem; S : Set Elem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova. let (var S : Set Elem) =

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova (op MultiSetToSet[Elem] :

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova forall Elem : Type . MultiSet Elem -> Set Elem)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova (var B : MultiSet Elem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova forall x : Elem .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __isIn__[Elem] : forall S : Type . S * Set S ->? Unit)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ((var x : Elem), (var S : Set Elem))

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova <=>

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova (pred __>__ : Nat * Nat)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ((op freq[Elem] :

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova forall Elem : Type . Elem * MultiSet Elem -> Nat)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova ((var x : Elem), (var B : MultiSet Elem)),

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova (op 0 : Nat))

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovavar S : Type

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovatype MapMultiSet : Type -> Type :=

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova \ S : Type . MultiSet S ->? MultiSet S

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovavar a : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaop sumN : (Nat ->? Nat) -> Nat -> Nat;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova sumSet : Set Nat ->? Nat;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova sum : (a ->? Nat) -> Pred a ->? Nat

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovavar S : Type; V : Type; U : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovatype Map : Type -> Type := \ S : Type . S ->? S

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaop dom : (S ->? V) -> Set S;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova range : (S ->? V) -> Set V;

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova image : (S ->? V) -> Set S -> Set V;

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova emptyMap : (S ->? V);

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova __::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova __[__/__] : (S ->? V) * S * V -> (S ->? V);

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova __-__ : (S ->? V) * S -> (S ->? V);

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova __o__ : (V ->? U) * (S ->? V) -> (S ->? U);

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova __||__ : (S ->? V) * Set S -> (S ->? V);

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova undef__ : S ->? V;

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova ker : (S ->? V) -> Pred (S * S);

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova injective : Pred (S ->? V);

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova __intersectionMap__, __unionMap__ : (S ->? V) * (S ->? V) ->

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova (S ->? V);

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova __restrict__ : (S ->? V) * Set S -> (S ->? V)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovavar S : Type; V : Type

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova freeMap : Map S -> MapMultiSet S;

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop __intersection__ : MultiSet Elem * MultiSet Elem ->

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova MultiSet Elem, assoc, comm, idem

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovatype P, T

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovatype Net =

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova {(p, pre, post) : Set P * (T ->? MultiSet P) * (T ->? MultiSet P)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova .

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova (op dom[T; P ->? Nat] :

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova forall S : Type; V : Type . (S ->? V) -> Set S)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (var pre : T ->? MultiSet P)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova =

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova (op dom[T; P ->? Nat] :

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

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova (var post : T ->? MultiSet P)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova /\

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova (forall p1 : MultiSet P .

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova (op __isIn__[P ->? Nat] : forall S : Type . S * Set S ->? Unit)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova ((var p1 : MultiSet P),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op range[T; P ->? Nat] :

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova forall S : Type; V : Type . (S ->? V) -> Set V)

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova (var pre : T ->? MultiSet P))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __subset__[P] : forall S : Type . Pred (Set S * Set S))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((op MultiSetToSet[P] :

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova forall Elem : Type . MultiSet Elem -> Set Elem)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (var p1 : MultiSet P),

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (var p : Set P)))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova /\

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (forall p1 : MultiSet P .

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op __isIn__[P ->? Nat] : forall S : Type . S * Set S ->? Unit)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var p1 : MultiSet P),

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op range[T; P ->? Nat] :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova forall S : Type; V : Type . (S ->? V) -> Set V)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var pre : T ->? MultiSet P))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova =>

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op __subset__[P] : forall S : Type . Pred (Set S * Set S))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((op MultiSetToSet[P] :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova forall Elem : Type . MultiSet Elem -> Set Elem)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var p1 : MultiSet P),

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var p : Set P)))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova }

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovaop places : Net -> Set P;

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova transitions : Net -> Set T;

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova preMap, postMap : Net -> (T ->? MultiSet P)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovatype HomNet =

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova {(n1, hp, ht, n2) : Net * (P ->? P) * (T ->? T) * Net .

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op __::__-->__[P; P] :

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var hp : P ->? P), (op places : Net -> Set P) (var n1 : Net),

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op places : Net -> Set P) (var n2 : Net))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova /\

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op __::__-->__[T; T] :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var ht : T ->? T),

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

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op transitions : Net -> Set T) (var n2 : Net))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova /\

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (forall t : T .

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op __isIn__[T] : forall S : Type . S * Set S ->? Unit)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var t : T), (op transitions : Net -> Set T) (var n1 : Net))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova =>

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op freeMap[P] : forall S : Type . Map S -> MapMultiSet S)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var hp : P ->? P)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((op preMap : Net -> T ->? MultiSet P) (var n1 : Net) (var t : T))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova =

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op preMap : Net -> T ->? MultiSet P) (var n2 : Net)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var ht : T ->? T) (var t : T))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova /\

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op freeMap[P] : forall S : Type . Map S -> MapMultiSet S)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var hp : P ->? P)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((op postMap : Net -> T ->? MultiSet P) (var n1 : Net)

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova (var t : T))

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova =

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op postMap : Net -> T ->? MultiSet P) (var n2 : Net)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var ht : T ->? T) (var t : T)))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova }

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakovaop dom : HomNet -> Net;

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova cod : HomNet -> Net;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova placesMap : HomNet -> (P ->? P);

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova transitionsMap : HomNet -> (T ->? T);

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova id : Net ->? HomNet;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova __o__ : HomNet * HomNet ->? HomNet

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovapred injective : HomNet

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovatype Marking : Type := MultiSet P

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovatype System =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova {(n, m) : Net * Marking .

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova let ((var p : P ->? Unit), (var pre1 : T ->? P ->? Nat),

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (var post1 : T ->? P ->? Nat))

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova = (var n : Net)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova forall x : P .

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (op __isIn__[P] :

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

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var x : P), (var m : Marking))

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova =>

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (op __isIn__[P] : forall S : Type . S * Set S ->? Unit)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ((var x : P), (var p : P ->? Unit))

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova }

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovaop marking : System -> Marking;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova net : System -> Net;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova empty : Marking;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova __|<__> : System * T -> System;

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova __|<__> : System * MultiSet T ->? System

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakovatype HomSys =

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova {(sys1, hp, ht, sys2) : System * (P ->? P) * (T ->? T) * System .

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (((op net : System -> Net) (var sys1 : System),

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (var hp : P ->? P), (var ht : T ->? T),

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova (op net : System -> Net) (var sys2 : System))

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in HomNet)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova /\

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (forall p : P .

b470a3e54a4289b4189906e41f0c04578c85619dKristina Sojakova (pred __<=__ : Nat * Nat)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova ((var p : P),

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

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova (op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((var hp : P ->? P) (var p : P),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op marking : System -> Marking) (var sys2 : System))))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaop dom : HomSys -> System;

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova cod : HomSys -> System;

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova placesMap : HomSys -> (P ->? P);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova transitionsMap : HomSys -> (T ->? T);

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova id : System ->? HomSys;

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova __o__ : HomSys * HomSys ->? HomSys

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovapred injective : HomSys

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall h1 : HomSys; h2 : HomSys

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova. def

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __o__ : HomSys * HomSys ->? HomSys)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((var h2 : HomSys), (var h1 : HomSys))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __o__ : HomSys * HomSys ->? HomSys)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((var h2 : HomSys), (var h1 : HomSys))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova =

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova (((op dom : HomSys -> System) (var h1 : HomSys),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __o__[P; P; P] :

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova forall S : Type; V : Type; U : Type .

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova (V ->? U) * (S ->? V) -> S ->? U)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op placesMap : HomSys -> P ->? P) (var h1 : HomSys)),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op __o__[T; T; T] :

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova forall S : Type; V : Type; U : Type .

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova (V ->? U) * (S ->? V) -> S ->? U)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys)),

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op cod : HomSys -> System) (var h2 : HomSys))

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova as HomSys)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%% Type Constructors -----------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaBoolean

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova: Type

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova %[free type Boolean ::=

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova True : Boolean

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova False : Boolean]%

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaHomNet : Type := _t1018 Net (P ->? P) (T ->? T) Net

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaHomSys : Type := _t1516 System (P ->? P) (T ->? T) System

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaMap : Type -> Type := \ S : Type . S ->? S

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovaMapMultiSet

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova: Type -> Type := \ S : Type . MultiSet S ->? MultiSet S

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaMarking : Type := MultiSet P

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina SojakovaMultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaNat : Type

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaNet : Type := _t366 (Set P) (T ->? MultiSet P) (T ->? MultiSet P)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaP : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaSet : Type -> Type := \ S : Type . S ->? Unit

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaSystem : Type := _t1088 Net Marking

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovaT : Type

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova_t1015 : +Type -> Type := _t1018 Net (P ->? P) (T ->? T)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova_t1016 : +Type -> +Type -> Type := _t1018 Net (P ->? P)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova_t1017 : +Type -> +Type -> +Type -> Type := _t1018 Net

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova_t1018 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova_t1087 : +Type -> Type := _t1088 Net

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova_t1088 : +Type -> +Type -> Type < __*__

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova_t1513 : +Type -> Type := _t1516 System (P ->? P) (T ->? T)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova_t1514 : +Type -> +Type -> Type := _t1516 System (P ->? P)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova_t1515 : +Type -> +Type -> +Type -> Type := _t1516 System

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova_t1516 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova_t364 : +Type -> Type := _t366 (Set P) (T ->? MultiSet P)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova_t365 : +Type -> +Type -> Type := _t366 (Set P)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova_t366 : +Type -> +Type -> +Type -> Type < __*__*__

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova%% Type Variables --------------------------------------------------------

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaElem : Type %(var_6)%

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovaS : Type %(var_62)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaU : Type %(var_60)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaV : Type %(var_63)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaa : Type %(var_57)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%% Assumptions -----------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova0 : Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova1 : Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaFalse : Boolean %(construct Boolean)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaMultiSetToSet

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall Elem : Type . MultiSet Elem -> Set Elem %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaTrue : Boolean %(construct Boolean)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__*__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . Set S * Set V -> Set (S * V) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__+__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall Elem : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaMultiSet Elem * MultiSet Elem -> MultiSet Elem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: Nat * Nat -> Nat %(op)%

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova__-__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * S -> S ->? V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall Elem : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaMultiSet Elem * MultiSet Elem -> MultiSet Elem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: Nat * Nat -> Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__::__-->__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall S : Type; V : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaPred ((S ->? MultiSet V) * Set S * Set V)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__<=__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall Elem : Type . Pred (MultiSet Elem * MultiSet Elem) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: Nat * Nat ->? Unit %(pred)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__>__ : Nat * Nat ->? Unit %(pred)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__>=__ : Nat * Nat ->? Unit %(pred)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__[__/__]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * S * V -> S ->? V %(op)%

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__disjointUnion__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type . Set S * Set S -> Set (S * Boolean) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__intersection__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall Elem : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaMultiSet Elem * MultiSet Elem -> MultiSet Elem,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaassoc, comm, idem %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type . Set S * Set S -> Set S %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__intersectionMap__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * (S ->? V) -> S ->? V

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__isIn__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall Elem : Type . Pred (Elem * MultiSet Elem) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type . S * Set S ->? Unit %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__o__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys * HomSys ->? HomSys %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet * HomNet ->? HomNet %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall S : Type; V : Type; U : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova(V ->? U) * (S ->? V) -> S ->? U

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__restrict__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * Set S -> S ->? V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__subset__ : forall S : Type . Pred (Set S * Set S) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__union__ : forall S : Type . Set S * Set S -> Set S %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__unionMap__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * (S ->? V) -> S ->? V

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__|<__>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: System * MultiSet T ->? System %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: System * T -> System %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova__||__

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) * Set S -> S ->? V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovacod

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys -> System %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet -> Net %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadom

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys -> System %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet -> Net %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) -> Set S %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaempty : Marking %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaemptyMap : forall S : Type; V : Type . S ->? V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaemptySet : forall S : Type . Set S %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovafreeMap : forall S : Type . Map S -> MapMultiSet S %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovafreq : forall Elem : Type . Elem * MultiSet Elem -> Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaid

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: System ->? HomSys %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: Net ->? HomNet %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimage

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . (S ->? V) -> Set S -> Set V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainjective

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys ->? Unit %(pred)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet ->? Unit %(pred)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type; V : Type . Pred (S ->? V) %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainjl : forall S : Type . S -> S * Boolean %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainjr : forall S : Type . S -> S * Boolean %(op)%

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalinMap

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall S : Type; V : Type .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova(S ->? MultiSet V) -> MultiSet S ->? MultiSet V

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamarking : System -> Marking %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamin : Nat * Nat -> Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovanet : System -> Net %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaplaces : Net -> Set P %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaplacesMap

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys -> P ->? P %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet -> P ->? P %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovapostMap : Net -> T ->? MultiSet P %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovapreMap : Net -> T ->? MultiSet P %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovarange : forall S : Type; V : Type . (S ->? V) -> Set V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasetToMultiSet

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall Elem : Type . Set Elem -> MultiSet Elem %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovasum : forall a : Type . (a ->? Nat) -> Pred a ->? Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasumN : (Nat ->? Nat) -> Nat -> Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasumSet : Set Nat ->? Nat %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovatransitions : Net -> Set T %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatransitionsMap

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomSys -> T ->? T %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: HomNet -> T ->? T %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaundef__ : forall S : Type; V : Type . S ->? V %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova{__}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall Elem : Type . Elem -> MultiSet Elem %(op)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova: forall S : Type . S -> Set S %(op)%

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

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova%% Variables -------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaB : MultiSet Elem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaS : Set Elem

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovah1 : HomSys

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovah2 : HomSys

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%% Sentences -------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovafree type Boolean ::=

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova True : Boolean

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova False : Boolean %(ga_Boolean)%

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovalet S = MultiSetToSet B in

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaforall x : Elem .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova(__isIn__ : Elem * Set Elem ->? Unit) (x, S) <=>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova((freq (x, B)) > 0)

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

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova(((op dom : HomSys -> System) h1,

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (__o__ : (P ->? P) * (P ->? P) -> P ->? P)

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

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (__o__ : (T ->? T) * (T ->? T) -> T ->? T)

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

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (op cod : HomSys -> System) h2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova as HomSys)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%% Diagnostics -----------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 7.7, is type variable 'S'

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

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova### Hint 8.12, rebound type variable 'S'

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

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova### Hint 20.18, rebound type variable 'Elem'

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

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

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

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

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

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova### Hint 34.12, rebound variable 'S'

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova### Hint 34.12, rebound variable 'S'

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

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

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

### Hint 38.21, 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 46.12, rebound type variable 'S'

### 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 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[_v161; _v173 _v174 _v172] :

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

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

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

(op range[_v276; _v288 _v289 _v287] :

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

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

### 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 '_v381 ->? Nat' (63.47)

### 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 '_v555 ->? Nat' (63.47)

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

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

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

### 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__[P] :

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

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

=>

((op __isIn__[_v1069] :

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[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)

((var p : P),

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

(op freq[P] : 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 ->? Nat' (23.33)

### 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, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__'

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

### 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, in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__'

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

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

typename '_t1088' (93.8)

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

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

typename '__->?__'

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

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

### 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 '_t1516 System (P ->? P)' (102.54)

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

### 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 '_t1018 Net (P ->? P)' (79.35)

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

### 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 '_t1516 System (P ->? P)' (102.54)

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

### 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 '_t1018 Net (P ->? P)' (79.35)

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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

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

typename '_t1088' (93.8)

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