047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop 0, 1 : Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop __+__, __-__, min : Nat * Nat -> Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskipred __>=__, __<=__, __>__ : Nat * Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskifree type Boolean ::= True |

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski False

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar S : Type; V : Type

601dc92e4c128d23a726593357c654fb776a63a7Till Mossakowskitype Set : Type -> Type := \ S : Type . S_v-1 ->? Unit

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop emptySet : Set S; {__} : S -> Set S;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __isIn__ : S * Set S ->? Unit;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __subset__ : Pred (Set (S) * Set (S));

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __union__, __intersection__, __\\__ : Set S * Set S -> Set S;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __disjoint__ : Pred (Set (S) * Set (S));

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __*__ : Set S * Set V -> Set (S * V);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __disjointUnion__ : Set S * Set S -> Set (S * Boolean);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski injl, injr : S -> S * Boolean

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar Elem : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype MultiSet : Type -> Type := \ Elem : Type . Elem_v-1 ->? Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop __isIn__ : Pred (Elem * MultiSet Elem);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __<=__ : Pred (MultiSet Elem * MultiSet Elem); {} : MultiSet Elem;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski {__} : Elem -> MultiSet Elem;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __+__, __-__, __intersection__ : MultiSet Elem *

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski MultiSet Elem -> MultiSet Elem;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski freq : Elem * MultiSet Elem -> Nat;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski setToMultiSet : Set Elem -> MultiSet Elem

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar Elem : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop MultiSetToSet : MultiSet Elem -> Set Elem

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiforall B : MultiSet Elem@(Elem ->? Nat);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski S : Set Elem@(Elem ->? Unit)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski. let (var S : Set Elem@(Elem ->? Unit)) =

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski ((op MultiSetToSet[Elem]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall Elem : Type .

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski MultiSet Elem@(Elem ->? Nat) -> Set Elem@(Elem ->? Unit))

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (var B : MultiSet Elem@(Elem ->? Nat)) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Set Elem@(Elem ->? Unit)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski in forall x : Elem

da955132262baab309a50fdffe228c9efe68251dCui Jian . (fun __<=>__ : ? Unit * ? Unit ->? Unit)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (((op __isIn__[Elem]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Elem * Set Elem@(Elem ->? Unit) ->? Unit)

da955132262baab309a50fdffe228c9efe68251dCui Jian (var x : Elem, var S : Set Elem@(Elem ->? Unit)) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Unit,

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (pred __>__ : Nat * Nat)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (((op freq[Elem]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall Elem : Type .

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Elem_v-1 * MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

da955132262baab309a50fdffe228c9efe68251dCui Jian Elem * MultiSet Elem@(Elem ->? Nat) -> Nat)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (var x : Elem, var B : MultiSet Elem@(Elem ->? Nat)) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Nat,

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski op 0 : Nat) :

da955132262baab309a50fdffe228c9efe68251dCui Jian Unit) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Unit

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar S : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype MapMultiSet : Type -> Type := \ S : Type . MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar a : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop sumN : (Nat ->? Nat) -> Nat -> Nat; sumSet : Set Nat ->? Nat;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski sum : (a ->? Nat) -> Pred a ->? Nat

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskivar S : Type; V : Type; U : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype Map : Type -> Type := \ S : Type . S_v-1 ->? S_v-1

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop dom : (S ->? V) -> Set S; range : (S ->? V) -> Set V;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski image : (S ->? V) -> Set S -> Set V; emptyMap : (S ->? V);

da955132262baab309a50fdffe228c9efe68251dCui Jian __::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __[__/__] : (S ->? V) * S * V -> (S ->? V);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __-__ : (S ->? V) * S -> (S ->? V);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __o__ : (V ->? U) * (S ->? V) -> (S ->? U);

da955132262baab309a50fdffe228c9efe68251dCui Jian __||__ : (S ->? V) * Set S -> (S ->? V); undef__ : S ->? V;

da955132262baab309a50fdffe228c9efe68251dCui Jian ker : (S ->? V) -> Pred (S * S); injective : Pred (S ->? V);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski __intersectionMap__, __unionMap__ : (S ->? V) *

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (S ->? V) -> (S ->? V);

da955132262baab309a50fdffe228c9efe68251dCui Jian __restrict__ : (S ->? V) * Set S -> (S ->? V)

da955132262baab309a50fdffe228c9efe68251dCui Jianvar S : Type; V : Type

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski freeMap : Map S -> MapMultiSet S;

da955132262baab309a50fdffe228c9efe68251dCui Jian linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiop __intersection__ : MultiSet Elem * MultiSet Elem -> MultiSet

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Elem, assoc, comm, idem

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype P, T

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype Net = {(p, pre, post) : Set P@(P ->? Unit) *

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (T ->? MultiSet P@(P ->? Nat)) *

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (T ->? MultiSet P@(P ->? Nat)) . (fun __/\__

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : ? Unit * ? Unit ->? Unit)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski ((fun __/\__

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : ? Unit * ? Unit ->? Unit)

da955132262baab309a50fdffe228c9efe68251dCui Jian (((fun __=__[T ->? Unit]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall a : Type .

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski a_v-1 * a_v-1 ->? Unit) :

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (T ->? Unit) *

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (T ->? Unit) ->? Unit)

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (((op dom[T; P ->? Nat]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall S : Type;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski V : Type .

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit)) :

da955132262baab309a50fdffe228c9efe68251dCui Jian (T ->? P ->? Nat) -> Set T@(T ->? Unit))

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (var pre : T ->? MultiSet P@(P ->? Nat)) :

da955132262baab309a50fdffe228c9efe68251dCui Jian Set T@(T ->? Unit),

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski ((op dom[T; P ->? Nat]

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski : forall S : Type;

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski V : Type .

047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit)) :

(T ->? P ->? Nat) -> Set T@(T ->? Unit))

(var post : T ->? MultiSet P@(P ->? Nat)) :

Set T@(T ->? Unit)) :

Unit,

forall p1 : MultiSet P@(P ->? Nat)

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[P ->? Nat]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

(P ->? Nat) *

Set (P ->? Nat)@((P ->? Nat) ->? Unit) ->? Unit)

(var p1 : MultiSet P@(P ->? Nat),

((op range[T;

P ->? Nat]

: forall S : Type;

V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(T ->? P ->? Nat) -> Set (P ->? Nat)@((P ->? Nat) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (P ->? Nat)@((P ->? Nat) ->? Unit)) :

Unit,

((op __subset__[P]

: forall S : Type .

Pred (Set S_v-1 *

Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)) :

Pred (Set P *

Set P)@(Set P@(P ->? Unit) *

Set P@(P ->? Unit) ->? Unit))

(((op MultiSetToSet[P]

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

MultiSet P@(P ->? Nat) -> Set P@(P ->? Unit))

(var p1 : MultiSet P@(P ->? Nat)) :

Set P@(P ->? Unit),

var p : Set P@(P ->? Unit)) :

Unit) :

Unit) :

Unit,

forall p1 : MultiSet P@(P ->? Nat)

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[P ->? Nat]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

(P ->? Nat) *

Set (P ->? Nat)@((P ->? Nat) ->? Unit) ->? Unit)

(var p1 : MultiSet P@(P ->? Nat),

((op range[T; P ->? Nat]

: forall S : Type;

V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(T ->? P ->? Nat) -> Set (P ->? Nat)@((P ->? Nat) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (P ->? Nat)@((P ->? Nat) ->? Unit)) :

Unit,

((op __subset__[P]

: forall S : Type .

Pred (Set S_v-1 *

Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)) :

Pred (Set P *

Set P)@(Set P@(P ->? Unit) *

Set P@(P ->? Unit) ->? Unit))

(((op MultiSetToSet[P]

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

MultiSet P@(P ->? Nat) -> Set P@(P ->? Unit))

(var p1 : MultiSet P@(P ->? Nat)) :

Set P@(P ->? Unit),

var p : Set P@(P ->? Unit)) :

Unit) :

Unit) :

Unit}

op places : Net -> Set P; transitions : Net -> Set T;

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

type HomNet = {(n1, hp, ht, n2) : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) . (fun __/\__

: ? Unit *

? Unit ->? Unit)

((fun __/\__

: ? Unit *

? Unit ->? Unit)

(((op __::__-->__[P;

P]

: forall S : Type;

V : Type .

Pred ((S_v-1 ->? V_v-2) *

Pred S_v-1 *

Pred V_v-2)@((S_v-1 ->? V_v-2) *

Pred S_v-1@(S_v-1 ->? Unit) *

Pred V_v-2@(V_v-2 ->? Unit) ->? Unit)) :

Pred ((P ->? P) *

Pred P *

Pred P)@((P ->? P) *

Pred P@(P ->? Unit) *

Pred P@(P ->? Unit) ->? Unit))

(var hp : P ->? P,

(op places

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit),

(op places

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit)) :

Unit,

((op __::__-->__[T;

T]

: forall S : Type;

V : Type .

Pred ((S_v-1 ->? V_v-2) *

Pred S_v-1 *

Pred V_v-2)@((S_v-1 ->? V_v-2) *

Pred S_v-1@(S_v-1 ->? Unit) *

Pred V_v-2@(V_v-2 ->? Unit) ->? Unit)) :

Pred ((T ->? T) *

Pred T *

Pred T)@((T ->? T) *

Pred T@(T ->? Unit) *

Pred T@(T ->? Unit) ->? Unit))

(var ht : T ->? T,

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit),

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit)) :

Unit) :

Unit,

forall t : T

. (fun __=>__

: ? Unit *

? Unit ->? Unit)

(((op __isIn__[T]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

T *

Set T@(T ->? Unit) ->? Unit)

(var t : T,

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit)) :

Unit,

(fun __/\__

: ? Unit *

? Unit ->? Unit)

(((fun __=__[P ->? Nat]

: forall a : Type .

a_v-1 *

a_v-1 ->? Unit) :

(P ->? Nat) *

(P ->? Nat) ->? Unit)

((((op freeMap[P]

: forall S : Type .

Map S_v-1@(S_v-1 ->? S_v-1) -> MapMultiSet S_v-1@(MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat))) :

Map P@(P ->? P) -> MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(var hp : P ->? P) :

MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(((op preMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

(var t : T) :

MultiSet P@(P ->? Nat)) :

P ->? Nat,

((op preMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

((var ht : T ->? T)

(var t : T) :

T) :

MultiSet P@(P ->? Nat)) :

Unit,

((fun __=__[P ->? Nat]

: forall a : Type .

a_v-1 *

a_v-1 ->? Unit) :

(P ->? Nat) *

(P ->? Nat) ->? Unit)

((((op freeMap[P]

: forall S : Type .

Map S_v-1@(S_v-1 ->? S_v-1) -> MapMultiSet S_v-1@(MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat))) :

Map P@(P ->? P) -> MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(var hp : P ->? P) :

MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(((op postMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

(var t : T) :

MultiSet P@(P ->? Nat)) :

P ->? Nat,

((op postMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

((var ht : T ->? T)

(var t : T) :

T) :

MultiSet P@(P ->? Nat)) :

Unit) :

Unit) :

Unit) :

Unit}

op 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 : Type := MultiSet P@(P ->? Nat)

type System = {(n, m) : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)) . let (var p : P ->? Unit,

var pre1 : T ->? P ->? Nat,

var post1 : T ->? P ->? Nat)

= (var n : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

in forall x : P

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[P]

: forall Elem : Type .

Pred (Elem_v-1 *

MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (P * MultiSet P)@(P *

MultiSet P@(P ->? Nat) ->? Unit))

(var x : P,

var m : Marking@(MultiSet P@(P ->? Nat))) :

Unit,

((op __isIn__[P]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

P *

Set P@(P ->? Unit) ->? Unit)

(var x : P,

var p : P ->? Unit) :

Unit) :

Unit}

op marking : System -> Marking; net : System -> Net;

empty : Marking; __|<__> : System * T -> System;

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

type HomSys = {(sys1, hp, ht,

sys2) : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) . (fun __/\__

: ? Unit * ? Unit ->? Unit)

(((op net

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

(var sys1 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))),

var hp : P ->? P,

var ht : T ->? T,

(op net

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

(var sys2 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) in

HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) *

(T ->? T) *

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))),

forall p : P

. (pred __<=__ : Nat * Nat)

(((op freq[P]

: forall Elem : Type .

Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

P *

MultiSet P@(P ->? Nat) -> Nat)

(var p : P,

(op marking

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Marking@(MultiSet P@(P ->? Nat)))

(var sys1 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Marking@(MultiSet P@(P ->? Nat))) :

Nat,

((op freq[P]

: forall Elem : Type .

Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

P *

MultiSet P@(P ->? Nat) -> Nat)

((var hp : P ->? P)

(var p : P) :

P,

(op marking

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Marking@(MultiSet P@(P ->? Nat)))

(var sys2 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Marking@(MultiSet P@(P ->? Nat))) :

Nat) :

Unit) :

Unit}

op 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 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))));

h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

. (fun __=>__ : ? Unit * ? Unit ->? Unit)

(((fun def__[(((P ->? Unit) * (T ->? P ->? Nat) *

(T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))]

: forall a : Type . a_v-1 ->? Unit) :

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) ->? Unit)

((op __o__

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) *

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

Unit,

((fun __=__[(((P ->? Unit) * (T ->? P ->? Nat) *

(T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))]

: forall a : Type . a_v-1 * a_v-1 ->? Unit) :

((((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))) *

((((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))) ->? Unit)

((op __o__

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) *

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

((op dom

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))),

((op __o__[P; P; P]

: forall V : Type; U : Type; S : Type .

(V_v-1 ->? U_v-2) * (S_v-3 ->? V_v-1) -> S_v-3 ->? U_v-2) :

(P ->? P) * (P ->? P) -> P ->? P)

((op placesMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> P ->? P)

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

P ->? P,

(op placesMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> P ->? P)

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

P ->? P) :

P ->? P,

((op __o__[T; T; T]

: forall V : Type; U : Type; S : Type .

(V_v-1 ->? U_v-2) * (S_v-3 ->? V_v-1) -> S_v-3 ->? U_v-2) :

(T ->? T) * (T ->? T) -> T ->? T)

((op transitionsMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> T ->? T)

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

T ->? T,

(op transitionsMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> T ->? T)

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

T ->? T) :

T ->? T,

(op cod

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) as

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

Unit) :

Unit

%% Type Constructors -----------------------------------------------------

Boolean

: Type

%[free type Boolean

::= True : Boolean

False : Boolean]%

Elem : Type %(var_3)%

HomNet

: Type < Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))

= {(n1, hp, ht, n2) : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) . (fun __/\__

: ? Unit * ? Unit ->? Unit)

((fun __/\__

: ? Unit * ? Unit ->? Unit)

(((op __::__-->__[P; P]

: forall S : Type;

V : Type .

Pred ((S_v-1 ->? V_v-2) *

Pred S_v-1 *

Pred V_v-2)@((S_v-1 ->? V_v-2) *

Pred S_v-1@(S_v-1 ->? Unit) *

Pred V_v-2@(V_v-2 ->? Unit) ->? Unit)) :

Pred ((P ->? P) *

Pred P *

Pred P)@((P ->? P) *

Pred P@(P ->? Unit) *

Pred P@(P ->? Unit) ->? Unit))

(var hp : P ->? P,

(op places

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit),

(op places

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit)) :

Unit,

((op __::__-->__[T; T]

: forall S : Type;

V : Type .

Pred ((S_v-1 ->? V_v-2) *

Pred S_v-1 *

Pred V_v-2)@((S_v-1 ->? V_v-2) *

Pred S_v-1@(S_v-1 ->? Unit) *

Pred V_v-2@(V_v-2 ->? Unit) ->? Unit)) :

Pred ((T ->? T) *

Pred T *

Pred T)@((T ->? T) *

Pred T@(T ->? Unit) *

Pred T@(T ->? Unit) ->? Unit))

(var ht : T ->? T,

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit),

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit)) :

Unit) :

Unit,

forall t : T

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[T]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

T *

Set T@(T ->? Unit) ->? Unit)

(var t : T,

(op transitions

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit)) :

Unit,

(fun __/\__

: ? Unit *

? Unit ->? Unit)

(((fun __=__[P ->? Nat]

: forall a : Type .

a_v-1 *

a_v-1 ->? Unit) :

(P ->? Nat) *

(P ->? Nat) ->? Unit)

((((op freeMap[P]

: forall S : Type .

Map S_v-1@(S_v-1 ->? S_v-1) -> MapMultiSet S_v-1@(MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat))) :

Map P@(P ->? P) -> MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(var hp : P ->? P) :

MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(((op preMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

(var t : T) :

MultiSet P@(P ->? Nat)) :

P ->? Nat,

((op preMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

((var ht : T ->? T)

(var t : T) :

T) :

MultiSet P@(P ->? Nat)) :

Unit,

((fun __=__[P ->? Nat]

: forall a : Type .

a_v-1 *

a_v-1 ->? Unit) :

(P ->? Nat) *

(P ->? Nat) ->? Unit)

((((op freeMap[P]

: forall S : Type .

Map S_v-1@(S_v-1 ->? S_v-1) -> MapMultiSet S_v-1@(MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat))) :

Map P@(P ->? P) -> MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(var hp : P ->? P) :

MapMultiSet P@(MultiSet P@(P ->? Nat) ->? MultiSet P@(P ->? Nat)))

(((op postMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

(var t : T) :

MultiSet P@(P ->? Nat)) :

P ->? Nat,

((op postMap

: Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) :

T ->? MultiSet P@(P ->? Nat))

((var ht : T ->? T)

(var t : T) :

T) :

MultiSet P@(P ->? Nat)) :

Unit) :

Unit) :

Unit) :

Unit}

HomSys

: Type < System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))

= {(sys1, hp, ht, sys2) : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) . (fun __/\__

: ? Unit *

? Unit ->? Unit)

(((op net

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

(var sys1 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))),

var hp : P ->? P,

var ht : T ->? T,

(op net

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

(var sys2 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) in

HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) *

(T ->? T) *

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))),

forall p : P

. (pred __<=__

: Nat * Nat)

(((op freq[P]

: forall Elem : Type .

Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

P *

MultiSet P@(P ->? Nat) -> Nat)

(var p : P,

(op marking

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Marking@(MultiSet P@(P ->? Nat)))

(var sys1 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Marking@(MultiSet P@(P ->? Nat))) :

Nat,

((op freq[P]

: forall Elem : Type .

Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

P *

MultiSet P@(P ->? Nat) -> Nat)

((var hp : P ->? P)

(var p : P) :

P,

(op marking

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Marking@(MultiSet P@(P ->? Nat)))

(var sys2 : System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) :

Marking@(MultiSet P@(P ->? Nat))) :

Nat) :

Unit) :

Unit}

Logical : Type := Unit ->? Unit

Map : Type -> Type := \ S : Type . S_v-1 ->? S_v-1

MapMultiSet

: Type -> Type

:= \ S : Type . MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat)

Marking : Type := MultiSet P@(P ->? Nat)

MultiSet : Type -> Type := \ Elem : Type . Elem_v-1 ->? Nat

Nat : Type

Net

: Type < Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))

= {(p, pre, post) : Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)) . (fun __/\__

: ? Unit * ? Unit ->? Unit)

((fun __/\__ : ? Unit * ? Unit ->? Unit)

(((fun __=__[T ->? Unit]

: forall a : Type .

a_v-1 * a_v-1 ->? Unit) :

(T ->? Unit) *

(T ->? Unit) ->? Unit)

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

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit)) :

(T ->? P ->? Nat) -> Set T@(T ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set T@(T ->? Unit),

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

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit)) :

(T ->? P ->? Nat) -> Set T@(T ->? Unit))

(var post : T ->? MultiSet P@(P ->? Nat)) :

Set T@(T ->? Unit)) :

Unit,

forall p1 : MultiSet P@(P ->? Nat)

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[P ->? Nat]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

(P ->? Nat) *

Set (P ->? Nat)@((P ->? Nat) ->? Unit) ->? Unit)

(var p1 : MultiSet P@(P ->? Nat),

((op range[T; P ->? Nat]

: forall S : Type;

V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(T ->? P ->? Nat) -> Set (P ->? Nat)@((P ->? Nat) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (P ->? Nat)@((P ->? Nat) ->? Unit)) :

Unit,

((op __subset__[P]

: forall S : Type .

Pred (Set S_v-1 *

Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)) :

Pred (Set P *

Set P)@(Set P@(P ->? Unit) *

Set P@(P ->? Unit) ->? Unit))

(((op MultiSetToSet[P]

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

MultiSet P@(P ->? Nat) -> Set P@(P ->? Unit))

(var p1 : MultiSet P@(P ->? Nat)) :

Set P@(P ->? Unit),

var p : Set P@(P ->? Unit)) :

Unit) :

Unit) :

Unit,

forall p1 : MultiSet P@(P ->? Nat)

. (fun __=>__

: ? Unit * ? Unit ->? Unit)

(((op __isIn__[P ->? Nat]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

(P ->? Nat) *

Set (P ->? Nat)@((P ->? Nat) ->? Unit) ->? Unit)

(var p1 : MultiSet P@(P ->? Nat),

((op range[T; P ->? Nat]

: forall S : Type;

V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(T ->? P ->? Nat) -> Set (P ->? Nat)@((P ->? Nat) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (P ->? Nat)@((P ->? Nat) ->? Unit)) :

Unit,

((op __subset__[P]

: forall S : Type .

Pred (Set S_v-1 *

Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)) :

Pred (Set P *

Set P)@(Set P@(P ->? Unit) *

Set P@(P ->? Unit) ->? Unit))

(((op MultiSetToSet[P]

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

MultiSet P@(P ->? Nat) -> Set P@(P ->? Unit))

(var p1 : MultiSet P@(P ->? Nat)) :

Set P@(P ->? Unit),

var p : Set P@(P ->? Unit)) :

Unit) :

Unit) :

Unit}

P : Type

Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit

S : Type %(var_1)%

Set : Type -> Type := \ S : Type . S_v-1 ->? Unit

System

: Type < Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))

= {(n, m) : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)) . let (var p : P ->? Unit,

var pre1 : T ->? P ->? Nat,

var post1 : T ->? P ->? Nat)

= (var n : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

in forall x : P

. (fun __=>__ : ? Unit * ? Unit ->? Unit)

(((op __isIn__[P]

: forall Elem : Type .

Pred (Elem_v-1 *

MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (P * MultiSet P)@(P *

MultiSet P@(P ->? Nat) ->? Unit))

(var x : P,

var m : Marking@(MultiSet P@(P ->? Nat))) :

Unit,

((op __isIn__[P]

: forall S : Type .

S_v-1 *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

P * Set P@(P ->? Unit) ->? Unit)

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

Unit) :

Unit}

T : Type

U : Type %(var_35)%

Unit : Type

V : Type %(var_2)%

__*__ : +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

a : Type %(var_34)%

%% Assumptions -----------------------------------------------------------

0 : Nat %(op)%

1 : Nat %(op)%

False : Boolean %(construct Boolean)%

MultiSetToSet

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)

%(op)%

True : Boolean %(construct Boolean)%

__*__

: forall S : Type; V : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set V_v-2@(V_v-2 ->? Unit) -> Set (S_v-1 * V_v-2)@(S_v-1 *

V_v-2 ->? Unit)

%(op)%

__+__

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> MultiSet Elem_v-1@(Elem_v-1 ->? Nat)

%(op)%

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

__-__

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * S_v-1 -> S_v-1 ->? V_v-2

%(op)%

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> MultiSet Elem_v-1@(Elem_v-1 ->? Nat)

%(op)%

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

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__::__-->__

: forall S : Type; V : Type .

Pred ((S_v-1 ->? MultiSet V_v-2) * Set S_v-1 *

Set V_v-2)@((S_v-1 ->? MultiSet V_v-2@(V_v-2 ->? Nat)) *

Set S_v-1@(S_v-1 ->? Unit) * Set V_v-2@(V_v-2 ->? Unit) ->? Unit)

%(op)%

: forall S : Type; V : Type .

Pred ((S_v-1 ->? V_v-2) * Pred S_v-1 *

Pred V_v-2)@((S_v-1 ->? V_v-2) * Pred S_v-1@(S_v-1 ->? Unit) *

Pred V_v-2@(V_v-2 ->? Unit) ->? Unit)

%(op)%

__<=__

: forall Elem : Type .

Pred (MultiSet Elem_v-1 *

MultiSet Elem_v-1)@(MultiSet Elem_v-1@(Elem_v-1 ->? Nat) *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)

%(op)%

: Nat * Nat ->? Unit %(pred)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

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

__[__/__]

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * S_v-1 * V_v-2 -> S_v-1 ->? V_v-2

%(op)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__\\__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

__disjoint__

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

%(op)%

__disjointUnion__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set (S_v-1 * Boolean)@(S_v-1 *

Boolean ->? Unit)

%(op)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__intersection__

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> MultiSet Elem_v-1@(Elem_v-1 ->? Nat),assoc,

comm, idem

%(op)%

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

__intersectionMap__

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * (S_v-1 ->? V_v-2) -> S_v-1 ->? V_v-2

%(op)%

__isIn__

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)

%(op)%

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit

%(op)%

__o__

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) *

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

%(op)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) *

HomNet@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) ->? HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

%(op)%

: forall V : Type; U : Type; S : Type .

(V_v-1 ->? U_v-2) * (S_v-3 ->? V_v-1) -> S_v-3 ->? U_v-2

%(op)%

__restrict__

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * Set S_v-1@(S_v-1 ->? Unit) -> S_v-1 ->? V_v-2

%(op)%

__subset__

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

%(op)%

__union__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

__unionMap__

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * (S_v-1 ->? V_v-2) -> S_v-1 ->? V_v-2

%(op)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

__|<__>

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

MultiSet T@(T ->? Nat) ->? System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))

%(op)%

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

T -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))

%(op)%

__||__

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) * Set S_v-1@(S_v-1 ->? Unit) -> S_v-1 ->? V_v-2

%(op)%

bottom : forall a : Type . a_v-1 %(fun)%

cod

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))

%(op)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))

%(op)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

dom

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))

%(op)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))

%(op)%

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

empty : Marking@(MultiSet P@(P ->? Nat)) %(op)%

emptyMap : forall S : Type; V : Type . S_v-1 ->? V_v-2 %(op)%

emptySet : forall S : Type . Set S_v-1@(S_v-1 ->? Unit) %(op)%

false : Unit %(fun)%

freeMap

: forall S : Type .

Map S_v-1@(S_v-1 ->? S_v-1) -> MapMultiSet S_v-1@(MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet S_v-1@(S_v-1 ->? Nat))

%(op)%

freq

: forall Elem : Type .

Elem_v-1 * MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat

%(op)%

id

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

%(op)%

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) ->? HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))))

%(op)%

image

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set S_v-1@(S_v-1 ->? Unit) -> Set V_v-2@(V_v-2 ->? Unit)

%(op)%

injective

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? Unit

%(pred)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) ->? Unit

%(pred)%

: forall S : Type; V : Type .

Pred (S_v-1 ->? V_v-2)@((S_v-1 ->? V_v-2) ->? Unit)

%(op)%

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

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

ker

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Pred (S_v-1 * S_v-1)@(S_v-1 * S_v-1 ->? Unit)

%(op)%

linMap

: forall S : Type; V : Type .

(S_v-1 ->? MultiSet V_v-2@(V_v-2 ->? Nat)) -> MultiSet S_v-1@(S_v-1 ->? Nat) ->? MultiSet V_v-2@(V_v-2 ->? Nat)

%(op)%

marking

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Marking@(MultiSet P@(P ->? Nat))

%(op)%

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

net

: System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) -> Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))

%(op)%

not__ : ? Unit ->? Unit %(fun)%

places

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit)

%(op)%

placesMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> P ->? P

%(op)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) -> P ->? P

%(op)%

postMap

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat)

%(op)%

preMap

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> T ->? MultiSet P@(P ->? Nat)

%(op)%

range

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)

%(op)%

setToMultiSet

: forall Elem : Type .

Set Elem_v-1@(Elem_v-1 ->? Unit) -> MultiSet Elem_v-1@(Elem_v-1 ->? Nat)

%(op)%

sum

: forall a : Type .

(a_v-1 ->? Nat) -> Pred a_v-1@(a_v-1 ->? Unit) ->? Nat

%(op)%

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

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

transitions

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit)

%(op)%

transitionsMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> T ->? T

%(op)%

: HomNet@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat)))) -> T ->? T

%(op)%

true : Unit %(fun)%

undef__ : forall S : Type; V : Type . S_v-1 ->? V_v-2 %(op)%

{__}

: forall Elem : Type .

Elem_v-1 -> MultiSet Elem_v-1@(Elem_v-1 ->? Nat)

%(op)%

: forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit) %(op)%

{}

: forall Elem : Type . MultiSet Elem_v-1@(Elem_v-1 ->? Nat) %(op)%

�__ : ? Unit ->? Unit %(fun)%

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

free type Boolean

::= True : Boolean

False : Boolean %(ga_Boolean)%

let (var S : Set Elem@(Elem ->? Unit)) =

((op MultiSetToSet[Elem]

: forall Elem : Type .

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Set Elem_v-1@(Elem_v-1 ->? Unit)) :

MultiSet Elem@(Elem ->? Nat) -> Set Elem@(Elem ->? Unit))

(var B : MultiSet Elem@(Elem ->? Nat)) :

Set Elem@(Elem ->? Unit)

in forall x : Elem

. (fun __<=>__ : ? Unit * ? Unit ->? Unit)

(((op __isIn__[Elem]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit) :

Elem * Set Elem@(Elem ->? Unit) ->? Unit)

(var x : Elem, var S : Set Elem@(Elem ->? Unit)) :

Unit,

(pred __>__ : Nat * Nat)

(((op freq[Elem]

: forall Elem : Type .

Elem_v-1 * MultiSet Elem_v-1@(Elem_v-1 ->? Nat) -> Nat) :

Elem * MultiSet Elem@(Elem ->? Nat) -> Nat)

(var x : Elem, var B : MultiSet Elem@(Elem ->? Nat)) :

Nat,

op 0 : Nat) :

Unit) :

Unit

(fun __=>__ : ? Unit * ? Unit ->? Unit)

(((fun def__[(((P ->? Unit) * (T ->? P ->? Nat) *

(T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))]

: forall a : Type . a_v-1 ->? Unit) :

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) ->? Unit)

((op __o__

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) *

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

Unit,

((fun __=__[(((P ->? Unit) * (T ->? P ->? Nat) *

(T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))]

: forall a : Type . a_v-1 * a_v-1 ->? Unit) :

((((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))) *

((((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat)) *

(P ->? P) * (T ->? T) *

(((P ->? Unit) * (T ->? P ->? Nat) * (T ->? P ->? Nat)) *

(P ->? Nat))) ->? Unit)

((op __o__

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) *

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) ->? HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))),

((op dom

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))),

((op __o__[P; P; P]

: forall V : Type; U : Type; S : Type .

(V_v-1 ->? U_v-2) * (S_v-3 ->? V_v-1) -> S_v-3 ->? U_v-2) :

(P ->? P) * (P ->? P) -> P ->? P)

((op placesMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> P ->? P)

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

P ->? P,

(op placesMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> P ->? P)

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

P ->? P) :

P ->? P,

((op __o__[T; T; T]

: forall V : Type; U : Type; S : Type .

(V_v-1 ->? U_v-2) * (S_v-3 ->? V_v-1) -> S_v-3 ->? U_v-2) :

(T ->? T) * (T ->? T) -> T ->? T)

((op transitionsMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> T ->? T)

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

T ->? T,

(op transitionsMap

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> T ->? T)

(var h1 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

T ->? T) :

T ->? T,

(op cod

: HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) -> System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))

(var h2 : HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat)))) as

HomSys@(System@(Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))) *

(P ->? P) * (T ->? T) *

System@(Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) *

Marking@(MultiSet P@(P ->? Nat))))) :

Unit) :

Unit

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

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

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

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

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

*** Hint 31.6, redeclared type 'Elem'

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

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

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

*** Hint 34.12, variable shadows global name(s) 'S'

*** Hint 34.12, variable shadows global name(s) 'S'

*** Hint, rejected 'Unit < Nat' of '((op __isIn__[_var_13_v13]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (_var_13_v13 * MultiSet _var_13_v13)@(_var_13_v13 *

MultiSet _var_13_v13@(_var_13_v13 ->? Nat) ->? Unit))

(var x : Elem, var S : Set Elem@(Elem ->? Unit)) :

_var_12_v12'

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

*** Hint 37.7, redeclared type 'S'

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

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

*** Hint 45.7, redeclared type 'S'

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

*** Hint 45.9, redeclared type 'V'

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

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

*** Hint 62.7, redeclared type 'S'

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

*** Hint 62.10, redeclared type 'V'

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

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

*** Hint 72.45, rejected 'Unit < Nat' of '((op __isIn__[_var_83_v83]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (_var_83_v83 * MultiSet _var_83_v83)@(_var_83_v83 *

MultiSet _var_83_v83@(_var_83_v83 ->? Nat) ->? Unit))

(var p1 : MultiSet P@(P ->? Nat),

((op range[_var_95_v95; _var_101_v101 ->? _var_102_v102]

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(_var_95_v95 ->? _var_101_v101 ->? _var_102_v102) -> Set (_var_101_v101 ->? _var_102_v102)@((_var_101_v101 ->? _var_102_v102) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (_var_101_v101 ->? _var_102_v102)@((_var_101_v101 ->? _var_102_v102) ->? Unit)) :

_var_82_v82'

*** Hint 73.48, rejected 'Unit < Nat' of '((op __isIn__[_var_154_v154]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (_var_154_v154 * MultiSet _var_154_v154)@(_var_154_v154 *

MultiSet _var_154_v154@(_var_154_v154 ->? Nat) ->? Unit))

(var p1 : MultiSet P@(P ->? Nat),

((op range[_var_166_v166; _var_172_v172 ->? _var_173_v173]

: forall S : Type; V : Type .

(S_v-1 ->? V_v-2) -> Set V_v-2@(V_v-2 ->? Unit)) :

(_var_166_v166 ->? _var_172_v172 ->? _var_173_v173) -> Set (_var_172_v172 ->? _var_173_v173)@((_var_172_v172 ->? _var_173_v173) ->? Unit))

(var pre : T ->? MultiSet P@(P ->? Nat)) :

Set (_var_172_v172 ->? _var_173_v173)@((_var_172_v172 ->? _var_173_v173) ->? Unit)) :

_var_153_v153'

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

*** Hint 80.28-80.35, in type of '(var hp : P ->? P,

(op places

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit),

(op places

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set P@(P ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat)))) :

Set P@(P ->? Unit))'

typename 'P' (79.35)

is not unifiable with type '_var_238_v238 ->? _var_239_v239' (20.31)

*** Hint 80.66-80.78, in type of '(var ht : T ->? T,

(op transitions

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit),

(op transitions

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n2 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit))'

typename 'T' (79.45)

is not unifiable with type '_var_332_v332 ->? _var_333_v333' (20.31)

*** Hint 81.31, rejected 'Unit < Nat' of '((op __isIn__[_var_420_v420]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (_var_420_v420 * MultiSet _var_420_v420)@(_var_420_v420 *

MultiSet _var_420_v420@(_var_420_v420 ->? Nat) ->? Unit))

(var t : T,

(op transitions

: Net@(Set P@(P ->? Unit) * (T ->? MultiSet P@(P ->? Nat)) *

(T ->? MultiSet P@(P ->? Nat))) -> Set T@(T ->? Unit))

(var n1 : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat)))) :

Set T@(T ->? Unit)) :

_var_419_v419'

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

*** Hint, rejected 'Nat < Unit' of '(var x : P, var m : Marking@(MultiSet P@(P ->? Nat)))'

*** Hint 94.29-95.27, rejected 'Unit < Nat' of 'let (var p : _var_581_v581 ->? _var_582_v582,

var pre1 : _var_583_v583 ->? _var_585_v585 ->? _var_586_v586,

var post1 : _var_587_v587 ->? _var_589_v589 ->? _var_590_v590)

= (var n : Net@(Set P@(P ->? Unit) *

(T ->? MultiSet P@(P ->? Nat)) * (T ->? MultiSet P@(P ->? Nat))))

in forall x : P

. (fun __=>__ : ? Unit * ? Unit ->? Unit)

(((op __isIn__[P]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (P * MultiSet P)@(P * MultiSet P@(P ->? Nat) ->? Unit))

(var x : P, var m : Marking@(MultiSet P@(P ->? Nat))) :

Unit,

((op __isIn__[_var_608_v608]

: forall Elem : Type .

Pred (Elem_v-1 * MultiSet Elem_v-1)@(Elem_v-1 *

MultiSet Elem_v-1@(Elem_v-1 ->? Nat) ->? Unit)) :

Pred (_var_608_v608 * MultiSet _var_608_v608)@(_var_608_v608 *

MultiSet _var_608_v608@(_var_608_v608 ->? Nat) ->? Unit))

(var x : P, var p : _var_581_v581 ->? _var_582_v582) :

Unit) :