PetriSystemCategory.hascasl.output revision 9292a012760925eeb69ee23666f70592be6031b6
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop __+__, __-__, min : Nat * Nat -> Nat
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannpred __>=__, __<=__, __>__ : Nat * Nat
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannfree type Boolean ::= True | False
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannvar S : Type; V : Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype Set : Type -> Type := \ S : Type . S ->? Unit
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop emptySet : Set S;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {__} : S -> Set S;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __isIn__ : S * Set S ->? Unit;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __subset__ : Pred (Set (S) * Set (S));
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __union__, __intersection__, __\\__ : Set S * Set S -> Set S;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __disjoint__ : Pred (Set (S) * Set (S));
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __*__ : Set S * Set V -> Set (S * V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __disjointUnion__ : Set S * Set S -> Set (S * Boolean);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann injl, injr : S -> S * Boolean
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannvar Elem : Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype MultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop __isIn__ : Pred (Elem * MultiSet Elem);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __<=__ : Pred (MultiSet Elem * MultiSet Elem);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {} : MultiSet Elem;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {__} : Elem -> MultiSet Elem;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __+__, __-__, __intersection__ : MultiSet Elem * MultiSet Elem ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann MultiSet Elem;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann freq : Elem * MultiSet Elem -> Nat;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann setToMultiSet : Set Elem -> MultiSet Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannvar Elem : Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop MultiSetToSet : MultiSet Elem -> Set Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall B : MultiSet Elem; S : Set Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann. let (var S : Set Elem) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op MultiSetToSet[Elem] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall Elem : Type . MultiSet Elem -> Set Elem)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var B : MultiSet Elem)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall x : Elem .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[Elem] : forall S : Type . S * Set S ->? Unit)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var x : Elem), (var S : Set Elem))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (pred __>__ : Nat * Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op freq[Elem] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var x : Elem), (var B : MultiSet Elem)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op 0 : Nat))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype MapMultiSet : Type -> Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann := \ S : Type . MultiSet S ->? MultiSet S
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop sumN : (Nat ->? Nat) -> Nat -> Nat;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann sumSet : Set Nat ->? Nat;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann sum : (a ->? Nat) -> Pred a ->? Nat
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannvar S : Type; V : Type; U : Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype Map : Type -> Type := \ S : Type . S ->? S
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop dom : (S ->? V) -> Set S;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann range : (S ->? V) -> Set V;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann image : (S ->? V) -> Set S -> Set V;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann emptyMap : (S ->? V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __::__-->__ : Pred ((S ->? V) * Pred (S) * Pred (V));
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __[__/__] : (S ->? V) * S * V -> (S ->? V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __-__ : (S ->? V) * S -> (S ->? V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __o__ : (V ->? U) * (S ->? V) -> (S ->? U);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __||__ : (S ->? V) * Set S -> (S ->? V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann undef__ : S ->? V;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ker : (S ->? V) -> Pred (S * S);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann injective : Pred (S ->? V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __intersectionMap__, __unionMap__ : (S ->? V) * (S ->? V) ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __restrict__ : (S ->? V) * Set S -> (S ->? V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannvar S : Type; V : Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann freeMap : Map S -> MapMultiSet S;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann linMap : (S ->? MultiSet V) -> (MultiSet S ->? MultiSet V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop __intersection__ : MultiSet Elem * MultiSet Elem ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann MultiSet Elem, assoc, comm, idem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {(p, pre, post) : Set P * (T ->? MultiSet P) * (T ->? MultiSet P) .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op dom[T; P ->? Nat] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set S)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre : T ->? MultiSet P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op dom[T; P ->? Nat] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set S)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var post : T ->? MultiSet P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (forall p1 : MultiSet P .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[P ->? Nat] : forall S : Type . S * Set S ->? Unit)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op range[T; P ->? Nat] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre : T ->? MultiSet P))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __subset__[P] : forall S : Type . Pred (Set S * Set S))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op MultiSetToSet[P] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall Elem : Type . MultiSet Elem -> Set Elem)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var p : Set P)))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (forall p1 : MultiSet P .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[P ->? Nat] : forall S : Type . S * Set S ->? Unit)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op range[T; P ->? Nat] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre : T ->? MultiSet P))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __subset__[P] : forall S : Type . Pred (Set S * Set S))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op MultiSetToSet[P] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall Elem : Type . MultiSet Elem -> Set Elem)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var p : Set P)))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop places : Net -> Set P;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann transitions : Net -> Set T;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann preMap, postMap : Net -> (T ->? MultiSet P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {(n1, hp, ht, n2) : Net * (P ->? P) * (T ->? T) * Net .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __::__-->__[P; P] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var hp : P ->? P), (op places : Net -> Set P) (var n1 : Net),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op places : Net -> Set P) (var n2 : Net))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __::__-->__[T; T] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var ht : T ->? T),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitions : Net -> Set T) (var n1 : Net),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitions : Net -> Set T) (var n2 : Net))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (forall t : T .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[T] : forall S : Type . S * Set S ->? Unit)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var t : T), (op transitions : Net -> Set T) (var n1 : Net))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op freeMap[P] : forall S : Type . Map S -> MapMultiSet S)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var hp : P ->? P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op preMap : Net -> T ->? MultiSet P) (var n1 : Net) (var t : T))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op preMap : Net -> T ->? MultiSet P) (var n2 : Net)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var ht : T ->? T) (var t : T))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op freeMap[P] : forall S : Type . Map S -> MapMultiSet S)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var hp : P ->? P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op postMap : Net -> T ->? MultiSet P) (var n1 : Net) (var t : T))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op postMap : Net -> T ->? MultiSet P) (var n2 : Net)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var ht : T ->? T) (var t : T)))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop dom : HomNet -> Net;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann cod : HomNet -> Net;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann placesMap : HomNet -> (P ->? P);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann transitionsMap : HomNet -> (T ->? T);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann id : Net ->? HomNet;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __o__ : HomNet * HomNet ->? HomNet
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannpred injective : HomNet
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype Marking := MultiSet P
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {(n, m) : Net * Marking .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let ((var p : P ->? Unit), (var pre1 : T ->? P ->? Nat),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var post1 : T ->? P ->? Nat))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann = (var n : Net)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall x : P .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[P] : forall Elem : Type . Pred (Elem * MultiSet Elem))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var x : P), (var m : Marking))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __isIn__[P] : forall S : Type . S * Set S ->? Unit)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var x : P), (var p : P ->? Unit))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop marking : System -> Marking;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann net : System -> Net;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann empty : Marking;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __|<__> : System * T -> System;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __|<__> : System * MultiSet T ->? System
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann {(sys1, hp, ht, sys2) : System * (P ->? P) * (T ->? T) * System .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (((op net : System -> Net) (var sys1 : System), (var hp : P ->? P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var ht : T ->? T), (op net : System -> Net) (var sys2 : System))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (forall p : P .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (pred __<=__ : Nat * Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var p : P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op marking : System -> Marking) (var sys1 : System)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var hp : P ->? P) (var p : P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op marking : System -> Marking) (var sys2 : System))))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannop dom : HomSys -> System;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann cod : HomSys -> System;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann placesMap : HomSys -> (P ->? P);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann transitionsMap : HomSys -> (T ->? T);
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann id : System ->? HomSys;
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann __o__ : HomSys * HomSys ->? HomSys
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannpred injective : HomSys
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall h1 : HomSys; h2 : HomSys
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __o__ : HomSys * HomSys ->? HomSys)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var h2 : HomSys), (var h1 : HomSys))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __o__ : HomSys * HomSys ->? HomSys)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var h2 : HomSys), (var h1 : HomSys))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (((op dom : HomSys -> System) (var h1 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __o__[P; P; P] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type; U : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (V ->? U) * (S ->? V) -> S ->? U)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op placesMap : HomSys -> P ->? P) (var h1 : HomSys)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op __o__[T; T; T] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type; U : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (V ->? U) * (S ->? V) -> S ->? U)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op cod : HomSys -> System) (var h2 : HomSys))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Type Constructors -----------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann %[free type Boolean ::=
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann True : Boolean
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann False : Boolean]%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannHomNet : Type := _t1018 Net (P ->? P) (T ->? T) Net
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannHomSys : Type := _t1516 System (P ->? P) (T ->? T) System
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMap : Type -> Type := \ S : Type . S ->? S
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: Type -> Type := \ S : Type . MultiSet S ->? MultiSet S
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMarking : Type := MultiSet P
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMultiSet : Type -> Type := \ Elem : Type . Elem ->? Nat
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannNet : Type := _t366 (Set P) (T ->? MultiSet P) (T ->? MultiSet P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannSet : Type -> Type := \ S : Type . S ->? Unit
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannSystem : Type := _t1088 Net Marking
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1015 : +Type -> Type := _t1018 Net (P ->? P) (T ->? T)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1016 : +Type -> +Type -> Type := _t1018 Net (P ->? P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1017 : +Type -> +Type -> +Type -> Type := _t1018 Net
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1018 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1087 : +Type -> Type := _t1088 Net
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1088 : +Type -> +Type -> Type < __*__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1513 : +Type -> Type := _t1516 System (P ->? P) (T ->? T)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1514 : +Type -> +Type -> Type := _t1516 System (P ->? P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1515 : +Type -> +Type -> +Type -> Type := _t1516 System
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t1516 : +Type -> +Type -> +Type -> +Type -> Type < __*__*__*__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t364 : +Type -> Type := _t366 (Set P) (T ->? MultiSet P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t365 : +Type -> +Type -> Type := _t366 (Set P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann_t366 : +Type -> +Type -> +Type -> Type < __*__*__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Type Variables --------------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannElem : Type %(var_6)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannS : Type %(var_62)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannU : Type %(var_60)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannV : Type %(var_63)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanna : Type %(var_57)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Assumptions -----------------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann0 : Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann1 : Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannFalse : Boolean %(construct Boolean)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall Elem : Type . MultiSet Elem -> Set Elem %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannTrue : Boolean %(construct Boolean)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . Set S * Set V -> Set (S * V) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall Elem : Type . MultiSet Elem * MultiSet Elem -> MultiSet Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: Nat * Nat -> Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * S -> S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall Elem : Type . MultiSet Elem * MultiSet Elem -> MultiSet Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: Nat * Nat -> Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall S : Type; V : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannPred ((S ->? MultiSet V) * Set S * Set V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . Pred ((S ->? V) * Pred S * Pred V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall Elem : Type . Pred (MultiSet Elem * MultiSet Elem) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: Nat * Nat ->? Unit %(pred)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__>__ : Nat * Nat ->? Unit %(pred)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__>=__ : Nat * Nat ->? Unit %(pred)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * S * V -> S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__\\__ : forall S : Type . Set S * Set S -> Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__disjointUnion__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type . Set S * Set S -> Set (S * Boolean) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__intersection__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall Elem : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMultiSet Elem * MultiSet Elem -> MultiSet Elem,
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannassoc, comm, idem %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type . Set S * Set S -> Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__intersectionMap__
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * (S ->? V) -> S ->? V
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall Elem : Type . Pred (Elem * MultiSet Elem) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type . S * Set S ->? Unit %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys * HomSys ->? HomSys %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet * HomNet ->? HomNet %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall S : Type; V : Type; U : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(V ->? U) * (S ->? V) -> S ->? U
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * Set S -> S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__subset__ : forall S : Type . Pred (Set S * Set S) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann__union__ : forall S : Type . Set S * Set S -> Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * (S ->? V) -> S ->? V
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: System * MultiSet T ->? System %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: System * T -> System %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) * Set S -> S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys -> System %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet -> Net %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys -> System %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet -> Net %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) -> Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannempty : Marking %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannemptyMap : forall S : Type; V : Type . S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannemptySet : forall S : Type . Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannfreeMap : forall S : Type . Map S -> MapMultiSet S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannfreq : forall Elem : Type . Elem * MultiSet Elem -> Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: System ->? HomSys %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: Net ->? HomNet %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . (S ->? V) -> Set S -> Set V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys ->? Unit %(pred)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet ->? Unit %(pred)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type; V : Type . Pred (S ->? V) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninjl : forall S : Type . S -> S * Boolean %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninjr : forall S : Type . S -> S * Boolean %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannker : forall S : Type; V : Type . (S ->? V) -> Pred (S * S) %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall S : Type; V : Type .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(S ->? MultiSet V) -> MultiSet S ->? MultiSet V
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannmarking : System -> Marking %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannmin : Nat * Nat -> Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannnet : System -> Net %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannplaces : Net -> Set P %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys -> P ->? P %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet -> P ->? P %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannpostMap : Net -> T ->? MultiSet P %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannpreMap : Net -> T ->? MultiSet P %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannrange : forall S : Type; V : Type . (S ->? V) -> Set V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall Elem : Type . Set Elem -> MultiSet Elem %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannsum : forall a : Type . (a ->? Nat) -> Pred a ->? Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsumN : (Nat ->? Nat) -> Nat -> Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannsumSet : Set Nat ->? Nat %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntransitions : Net -> Set T %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanntransitionsMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomSys -> T ->? T %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: HomNet -> T ->? T %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannundef__ : forall S : Type; V : Type . S ->? V %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall Elem : Type . Elem -> MultiSet Elem %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann: forall S : Type . S -> Set S %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann{} : forall Elem : Type . MultiSet Elem %(op)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Variables -------------------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannB : MultiSet Elem
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Sentences -------------------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannfree type Boolean ::=
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann True : Boolean
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann False : Boolean %(ga_Boolean)%
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannlet S = MultiSetToSet B in
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall x : Elem .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(__isIn__ : Elem * Set Elem ->? Unit) (x, S) <=>
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann((freq (x, B)) > 0)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndef (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1) =>
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(op __o__ : HomSys * HomSys ->? HomSys) (h2, h1) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(((op dom : HomSys -> System) h1,
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (__o__ : (P ->? P) * (P ->? P) -> P ->? P)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op placesMap : HomSys -> P ->? P) h2,
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op placesMap : HomSys -> P ->? P) h1),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (__o__ : (T ->? T) * (T ->? T) -> T ->? T)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((op transitionsMap : HomSys -> T ->? T) h2,
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitionsMap : HomSys -> T ->? T) h1),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op cod : HomSys -> System) h2)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann%% Diagnostics -----------------------------------------------------------
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 7.7, is type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 7.9, is type variable 'V'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 8.12, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 19.7, is type variable 'Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 20.18, rebound type variable 'Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 31.6, is type variable 'Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 31.6, rebound type variable 'Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 33.10, not a kind 'MultiSet Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 33.27, not a kind 'Set Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 35.17, not a class 'Elem'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 34.12, rebound variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 34.12, rebound variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, rejected 'Unit < Nat' of '((var x : Elem), (var S : Set Elem))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 37.7, is type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 37.7, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 38.21, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 40.7, is type variable 'a'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 45.7, is type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 45.7, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 45.9, is type variable 'V'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 45.9, rebound type variable 'V'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 45.11, is type variable 'U'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 46.12, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 62.7, is type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 62.7, rebound type variable 'S'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 62.10, is type variable 'V'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 62.10, rebound type variable 'V'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 72.23, not a kind 'MultiSet P'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 73.26, not a kind 'MultiSet P'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 72.45, rejected 'Unit < Nat' of '((var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op range[_v161; _v173 _v174 _v172] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre : T ->? MultiSet P))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 73.48, rejected 'Unit < Nat' of '((var p1 : MultiSet P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op range[_v276; _v288 _v289 _v287] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall S : Type; V : Type . (S ->? V) -> Set V)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre : T ->? MultiSet P))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 81.19, not a class 'T'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 80.14-80.35, in type of '((var hp : P ->? P), (op places : Net -> Set P) (var n1 : Net),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op places : Net -> Set P) (var n2 : Net))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename 'P' (79.35)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_v381 ->? Nat' (63.47)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 80.47-80.78, in type of '((var ht : T ->? T),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitions : Net -> Set T) (var n1 : Net),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitions : Net -> Set T) (var n2 : Net))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename 'T' (79.45)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_v555 ->? Nat' (63.47)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 81.31, rejected 'Unit < Nat' of '((var t : T), (op transitions : Net -> Set T) (var n1 : Net))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 95.38, not a class 'P'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, rejected 'Nat < Unit' of '((var x : P), (var m : Marking))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 94.29-95.62, rejected 'Unit < Nat' of 'let ((var p : _v1024 _v1025 _v1023),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var pre1 : _v1028 _v1029 (_v1032 _v1033 _v1031)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (var post1 : _v1036 _v1037 (_v1040 _v1041 _v1039)))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann = (var n : Net)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannforall x : P .
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(op __isIn__[P] : forall Elem : Type . Pred (Elem * MultiSet Elem))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann((var x : P), (var m : Marking))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann(op __isIn__[_v1069] :
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann forall Elem : Type . Pred (Elem * MultiSet Elem))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann((var x : P), (var p : _v1024 _v1025 _v1023))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 104.19, not a class 'P'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 104.24-104.74, in type of '((op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var p : P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op marking : System -> Marking) (var sys1 : System)),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op freq[P] : forall Elem : Type . Elem * MultiSet Elem -> Nat)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ((var hp : P ->? P) (var p : P),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op marking : System -> Marking) (var sys2 : System)))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename 'Nat' (28.38)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_v1288 ->? Nat' (23.33)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 112.12, not a class 'HomSys'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 112.16, not a class 'HomSys'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1516 System (P ->? P)' (102.54)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '((var h2 : HomSys), (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1516 System (P ->? P)' (102.54)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1516 System (P ->? P)' (102.54)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 114.15-114.40, in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1516 System (P ->? P)' (102.54)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 114.15-114.40, in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1018 Net (P ->? P)' (79.35)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 114.44-114.79, in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1516 System (P ->? P)' (102.54)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint 114.44-114.79, in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '__->?__'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t1018 Net (P ->? P)' (79.35)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h1 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann### Hint, in type of '(var h2 : HomSys)'
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann typename '_t1088' (93.8)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann is not unifiable with type '_t366 (Set P)' (71.34)