type Nat

ops 0, 1 : Nat

ops __+__, __-__, min : Nat * Nat -> Nat

preds __>=__, __<=__, __>__ : Nat * Nat

free type Boolean ::= True | False

vars S, V : Type

type Set S := S ->? Unit

ops emptySet : Set S;

{__} : S -> Set S;

__isIn__ : S * Set S ->? Unit;

__subset__ : Pred (Set (S) * Set (S));

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

__disjoint__ : Pred (Set (S) * Set (S));

__*__ : Set S * Set V -> Set (S * V);

__disjointUnion__ : Set S * Set S -> Set (S * Boolean);

injl, injr : S -> S * Boolean

var Elem : Type

type MultiSet Elem := Elem ->? Nat

ops __isIn__ : Pred (Elem * MultiSet Elem);

__<=__ : Pred (MultiSet Elem * MultiSet Elem);

{} : MultiSet Elem;

{__} : Elem -> MultiSet Elem;

__+__, __-__, __intersection__

: MultiSet Elem * MultiSet Elem -> MultiSet Elem;

freq : Elem * MultiSet Elem -> Nat;

setToMultiSet : Set Elem -> MultiSet Elem

var Elem : Type

op MultiSetToSet : MultiSet Elem -> Set Elem

forall B : MultiSet Elem; S : Set Elem

. let S = MultiSetToSet B in

forall x : Elem . x isIn S <=> freq (x, B) > 0;

var S : Type

type MapMultiSet S := MultiSet S ->? MultiSet S

var a : Type

ops sumN : (Nat ->? Nat) -> Nat -> Nat;

sumSet : Set Nat ->? Nat;

sum : (a ->? Nat) -> Pred a ->? Nat

vars S, V, U : Type

type Map S := S ->? S

ops dom : (S ->? V) -> Set S;

range : (S ->? V) -> Set V;

image : (S ->? V) -> Set S -> Set V;

emptyMap : (S ->? V);

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

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

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

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

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

undef__ : S ->? V;

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

injective : Pred (S ->? V);

__intersectionMap__, __unionMap__

: (S ->? V) * (S ->? V) -> (S ->? V);

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

vars S, V : Type

ops __::__-->__ : Pred ((S ->? MultiSet V) * Set S * Set V);

freeMap : Map S -> MapMultiSet S;

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

op __intersection__

: MultiSet Elem * MultiSet Elem -> MultiSet Elem, assoc, comm, idem

types P, T

type Net =

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

. (dom pre = dom post

/\ forall p1 : MultiSet P

. p1 isIn range pre => MultiSetToSet p1 subset p)

/\ forall p1 : MultiSet P

. p1 isIn range pre => MultiSetToSet p1 subset p

}

ops places : Net -> Set P;

transitions : Net -> Set T;

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

type HomNet =

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

. hp :: places n1 --> places n2

/\ ht :: transitions n1 --> transitions n2

/\ forall t : T

. t isIn transitions n1

=> freeMap hp (preMap n1 t) = preMap n2 (ht t)

/\ freeMap hp (postMap n1 t) = postMap n2 (ht t)

}

ops dom : HomNet -> Net;

cod : HomNet -> Net;

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

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

id : Net ->? HomNet;

__o__ : HomNet * HomNet ->? HomNet

pred injective : HomNet

type Marking := MultiSet P

type System =

{(n, m) : Net * Marking

. let (p, pre1, post1) = n in forall x : P . x isIn m => x isIn p

}

ops marking : System -> Marking;

net : System -> Net;

empty : Marking;

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

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

type HomSys =

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

. ((net sys1, hp, ht, net sys2) in HomNet)

/\ forall p : P

. freq (p, marking sys1) <= freq (hp p, marking sys2)

}

ops dom : HomSys -> System;

cod : HomSys -> System;

placesMap : HomSys -> (P ->? P);

transitionsMap : HomSys -> (T ->? T);

id : System ->? HomSys;

__o__ : HomSys * HomSys ->? HomSys

pred injective : HomSys

forall h1, h2 : HomSys

. def (h2 o h1)

=> h2 o h1

= ((dom h1, placesMap h2 o placesMap h1,

transitionsMap h2 o transitionsMap h1, cod h2)

as HomSys);

types

Boolean : Type;

HomNet : Type;

HomSys : Type;

Map : Type -> Type;

MapMultiSet : Type -> Type;

Marking : Type;

MultiSet : Type -> Type;

Nat : Type;

Net : Type;

P : Type;

Set : Type -> Type;

System : Type;

T : Type;

gn_t1007 : +Type -> Type;

gn_t1008 : +Type -> +Type -> Type;

gn_t1433 : +Type -> Type;

gn_t1434 : +Type -> +Type -> Type;

gn_t1435 : +Type -> +Type -> +Type -> Type;

gn_t1436 : +Type -> +Type -> +Type -> +Type -> Type;

gn_t300 : +Type -> Type;

gn_t301 : +Type -> +Type -> Type;

gn_t302 : +Type -> +Type -> +Type -> Type;

gn_t935 : +Type -> Type;

gn_t936 : +Type -> +Type -> Type;

gn_t937 : +Type -> +Type -> +Type -> Type;

gn_t938 : +Type -> +Type -> +Type -> +Type -> Type

types

gn_t1008 < __*__;

gn_t1436 < __*__*__*__;

gn_t302 < __*__*__;

gn_t938 < __*__*__*__

types

HomNet := gn_t935 Net;

HomSys := gn_t1433 System;

Map := \ S : Type . S ->? S;

MapMultiSet := \ S : Type . MultiSet S ->? MultiSet S;

Marking := MultiSet P;

MultiSet := \ Elem : Type . Elem ->? Nat;

Net := gn_t300 (T ->? MultiSet P);

Set := \ S : Type . S ->? Unit;

System := gn_t1007 Marking;

gn_t1007 := gn_t1008 Net;

gn_t1433 := gn_t1434 (T ->? T);

gn_t1434 := gn_t1435 (P ->? P);

gn_t1435 := gn_t1436 System;

gn_t300 := gn_t301 (T ->? MultiSet P);

gn_t301 := gn_t302 (Set P);

gn_t935 := gn_t936 (T ->? T);

gn_t936 := gn_t937 (P ->? P);

gn_t937 := gn_t938 Net

vars

Elem : Type %(var_6)%;

S : Type %(var_62)%;

U : Type %(var_60)%;

V : Type %(var_63)%;

a : Type %(var_57)%

op 0 : Nat %(op)%

op 1 : Nat %(op)%

op False : Boolean %(constructor)%

op MultiSetToSet : forall Elem : Type . MultiSet Elem -> Set Elem

%(op)%

op True : Boolean %(constructor)%

op __*__ : forall S : Type; V : Type . Set S * Set V -> Set (S * V)

%(op)%

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

op __+__ : forall Elem : Type

. MultiSet Elem * MultiSet Elem -> MultiSet Elem

%(op)%

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

op __-__ : forall Elem : Type

. MultiSet Elem * MultiSet Elem -> MultiSet Elem

%(op)%

op __-__ : forall S : Type; V : Type . (S ->? V) * S -> S ->? V

%(op)%

op __::__-->__ : forall S : Type; V : Type

. Pred ((S ->? V) * Pred S * Pred V)

%(op)%

op __::__-->__ : forall S : Type; V : Type

. Pred ((S ->? MultiSet V) * Set S * Set V)

%(op)%

op __<=__ : Nat * Nat ->? Unit %(pred)%

op __<=__ : forall Elem : Type

. Pred (MultiSet Elem * MultiSet Elem)

%(op)%

op __>__ : Nat * Nat ->? Unit %(pred)%

op __>=__ : Nat * Nat ->? Unit %(pred)%

op __[__/__] : forall S : Type; V : Type

. (S ->? V) * S * V -> S ->? V

%(op)%

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

op __disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%

op __disjointUnion__ : forall S : Type

. Set S * Set S -> Set (S * Boolean)

%(op)%

op __intersection__ : forall Elem : Type

. MultiSet Elem * MultiSet Elem -> MultiSet Elem

%(op)%

op __intersection__ : forall S : Type . Set S * Set S -> Set S

%(op)%

op __intersectionMap__ : forall S : Type; V : Type

. (S ->? V) * (S ->? V) -> S ->? V

%(op)%

op __isIn__ : forall S : Type . S * Set S ->? Unit %(op)%

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

%(op)%

op __o__ : HomSys * HomSys ->? HomSys %(op)%

op __o__ : HomNet * HomNet ->? HomNet %(op)%

op __o__ : forall S : Type; V : Type; U : Type

. (V ->? U) * (S ->? V) -> S ->? U

%(op)%

op __restrict__ : forall S : Type; V : Type

. (S ->? V) * Set S -> S ->? V

%(op)%

op __subset__ : forall S : Type . Pred (Set S * Set S) %(op)%

op __union__ : forall S : Type . Set S * Set S -> Set S %(op)%

op __unionMap__ : forall S : Type; V : Type

. (S ->? V) * (S ->? V) -> S ->? V

%(op)%

op __|<__> : System * T -> System %(op)%

op __|<__> : System * MultiSet T ->? System %(op)%

op __||__ : forall S : Type; V : Type

. (S ->? V) * Set S -> S ->? V

%(op)%

op cod : HomSys -> System %(op)%

op cod : HomNet -> Net %(op)%

op dom : HomSys -> System %(op)%

op dom : HomNet -> Net %(op)%

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

op empty : Marking %(op)%

op emptyMap : forall S : Type; V : Type . S ->? V %(op)%

op emptySet : forall S : Type . Set S %(op)%

op freeMap : forall S : Type . Map S -> MapMultiSet S %(op)%

op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat %(op)%

op id : System ->? HomSys %(op)%

op id : Net ->? HomNet %(op)%

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

%(op)%

op injective : HomSys ->? Unit %(pred)%

op injective : HomNet ->? Unit %(pred)%

op injective : forall S : Type; V : Type . Pred (S ->? V) %(op)%

op injl : forall S : Type . S -> S * Boolean %(op)%

op injr : forall S : Type . S -> S * Boolean %(op)%

op ker : forall S : Type; V : Type . (S ->? V) -> Pred (S * S)

%(op)%

op linMap : forall S : Type; V : Type

. (S ->? MultiSet V) -> MultiSet S ->? MultiSet V

%(op)%

op marking : System -> Marking %(op)%

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

op net : System -> Net %(op)%

op places : Net -> Set P %(op)%

op placesMap : HomSys -> P ->? P %(op)%

op placesMap : HomNet -> P ->? P %(op)%

op postMap : Net -> T ->? MultiSet P %(op)%

op preMap : Net -> T ->? MultiSet P %(op)%

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

op setToMultiSet : forall Elem : Type . Set Elem -> MultiSet Elem

%(op)%

op sum : forall a : Type . (a ->? Nat) -> Pred a ->? Nat %(op)%

op sumN : (Nat ->? Nat) -> Nat -> Nat %(op)%

op sumSet : Set Nat ->? Nat %(op)%

op transitions : Net -> Set T %(op)%

op transitionsMap : HomSys -> T ->? T %(op)%

op transitionsMap : HomNet -> T ->? T %(op)%

op undef__ : forall S : Type; V : Type . S ->? V %(op)%

op {__} : forall Elem : Type . Elem -> MultiSet Elem %(op)%

op {__} : forall S : Type . S -> Set S %(op)%

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

free type Boolean ::= False | True %(ga_Boolean)%

forall Elem : Type; B : MultiSet Elem

. let S = MultiSetToSet B in

forall x : Elem . x isIn S <=> freq (x, B) > 0

forall h1 : HomSys; h2 : HomSys

. def (op __o__ : HomSys * HomSys ->? HomSys) (h2, h1)

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

= (((op dom : HomSys -> System) h1,

(op placesMap : HomSys -> P ->? P) h2

o (op placesMap : HomSys -> P ->? P) h1,

(op transitionsMap : HomSys -> T ->? T) h2

o (op transitionsMap : HomSys -> T ->? T) h1,

(op cod : HomSys -> System) h2)

as HomSys)

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

### Hint 34.12, rebound variable 'S'

### Hint 35.25-35.32,

rejected 'Unit < Nat' of '((var x : Elem), (var S : Set Elem))'

### Hint 35.25-35.32,

untypable term (with type: _v21_Elem * MultiSet _v21_Elem)

'(x, S)'

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

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

### Hint 40.7, is type variable 'a'

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

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

### Hint 45.9, is type variable 'V'

### Hint 45.9, rebound type variable 'V'

### Hint 45.11, is type variable 'U'

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

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

### Hint 62.10, is type variable 'V'

### Hint 62.10, rebound type variable 'V'

### Hint 20.18-67.60,

repeated declaration of '__intersection__' with type

'MultiSet Elem * MultiSet Elem -> MultiSet Elem'

### Hint 72.23, not a kind 'MultiSet P'

### Hint 73.26, not a kind 'MultiSet P'

### Hint 72.37-72.51,

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

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

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

### Hint 72.37-72.51,

untypable term (with type: _v126_Elem * MultiSet _v126_Elem)

'(p1, range pre)'

### Hint 73.40-73.54,

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

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

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

### Hint 73.40-73.54,

untypable term (with type: _v217_Elem * MultiSet _v217_Elem)

'(p1, range pre)'

### Hint 81.19, not a class 'T'

### Hint 80.8-80.35,

in type of '((var hp : P ->? P), (op places : Net -> Set P) (var n1 : Net),

(op places : Net -> Set P) (var n2 : Net))'

typename 'P' (79.35)

is not unifiable with type '_v319_V ->? Nat' (63.47)

### Hint 80.8-80.35,

untypable term (with type: (_v318_S ->? MultiSet _v319_V) * Set _v318_S * Set _v319_V)

'(hp, places n1, places n2)'

### Hint 80.41-80.78,

in type of '((var ht : T ->? T),

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

(op transitions : Net -> Set T) (var n2 : Net))'

typename 'T' (79.45)

is not unifiable with type '_v493_V ->? Nat' (63.47)

### Hint 80.41-80.78,

untypable term (with type: (_v492_S ->? MultiSet _v493_V) * Set _v492_S * Set _v493_V)

'(ht, transitions n1, transitions n2)'

### Hint 81.24-81.43,

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

### Hint 81.24-81.43,

untypable term (with type: _v670_Elem * MultiSet _v670_Elem)

'(t, transitions n1)'

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

### Hint 95.43-95.50,

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

### Hint 95.43-95.50,

untypable term (with type: _v969_S * Set _v969_S)

'(x, m)'

### Hint 95.55-95.62,

rejected 'Unit < Nat' of '((var x : P), (var p : P ->? Unit))'

### Hint 95.55-95.62,

untypable term (with type: _v990_Elem * MultiSet _v990_Elem)

'(x, p)'

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

### Hint 104.24-104.74,

in type of '((op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)

((var p : P),

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

(op freq : forall Elem : Type . Elem * MultiSet Elem -> Nat)

((var hp : P ->? P) (var p : P),

(op marking : System -> Marking) (var sys2 : System)))'

typename 'Nat' (28.38)

is not unifiable with type '_v1208_Elem ->? Nat' (23.33)

### Hint 104.24-104.74,

untypable term (with type: MultiSet _v1208_Elem * MultiSet _v1208_Elem)

'(freq (p, marking sys1), freq (hp p, marking sys2))'

### Hint 112.12, not a class 'HomSys'

### Hint 112.16, not a class 'HomSys'

### Hint 113.10-113.15,

in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename 'gn_t1008' (93.8)

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

### Hint 113.10-113.15,

untypable term (with type: HomNet * HomNet)

'(h2, h1)'

### Hint 113.10-113.15,

in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__' (54.17)

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

### Hint 113.10-113.15,

untypable term (with type: (_v1446_V ->? _v1447_U) * (_v1448_S ->? _v1446_V))

'(h2, h1)'

### Hint 113.22-113.27,

in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename 'gn_t1008' (93.8)

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

### Hint 113.22-113.27,

untypable term (with type: HomNet * HomNet)

'(h2, h1)'

### Hint 113.22-113.27,

in type of '((var h2 : HomSys), (var h1 : HomSys))'

typename '__->?__' (54.17)

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

### Hint 113.22-113.27,

untypable term (with type: (_v1938_V ->? _v1939_U) * (_v1940_S ->? _v1938_V))

'(h2, h1)'

### Hint 114.11,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.11,

untypable term (with type: HomNet)

'h1'

### Hint 114.11,

in type of '(var h1 : HomSys)'

typename '__->?__' (47.15)

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

### Hint 114.11,

untypable term (with type: _v2424_S ->? _v2425_V)

'h1'

### Hint 114.25,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.25,

untypable term (with type: HomNet)

'h2'

### Hint 114.40,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.40,

untypable term (with type: HomNet)

'h1'

### Hint 114.15-114.40,

in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),

(op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'

typename '__->?__' (107.33)

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

### Hint 114.15-114.40,

untypable term (with type: HomSys * HomSys)

'(placesMap h2, placesMap h1)'

### Hint 114.25,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.25,

untypable term (with type: HomNet)

'h2'

### Hint 114.40,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.40,

untypable term (with type: HomNet)

'h1'

### Hint 114.15-114.40,

in type of '((op placesMap : HomSys -> P ->? P) (var h2 : HomSys),

(op placesMap : HomSys -> P ->? P) (var h1 : HomSys))'

typename '__->?__' (107.33)

is not unifiable with type 'gn_t937 (P ->? P)' (79.35)

### Hint 114.15-114.40,

untypable term (with type: HomNet * HomNet)

'(placesMap h2, placesMap h1)'

### Hint 114.25,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.25,

untypable term (with type: HomNet)

'h2'

### Hint 114.40,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.40,

untypable term (with type: HomNet)

'h1'

### Hint 114.59,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.59,

untypable term (with type: HomNet)

'h2'

### Hint 114.79,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.79,

untypable term (with type: HomNet)

'h1'

### Hint 114.44-114.79,

in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),

(op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'

typename '__->?__' (108.38)

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

### Hint 114.44-114.79,

untypable term (with type: HomSys * HomSys)

'(transitionsMap h2, transitionsMap h1)'

### Hint 114.59,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.59,

untypable term (with type: HomNet)

'h2'

### Hint 114.79,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.79,

untypable term (with type: HomNet)

'h1'

### Hint 114.44-114.79,

in type of '((op transitionsMap : HomSys -> T ->? T) (var h2 : HomSys),

(op transitionsMap : HomSys -> T ->? T) (var h1 : HomSys))'

typename '__->?__' (108.38)

is not unifiable with type 'gn_t937 (P ->? P)' (79.35)

### Hint 114.44-114.79,

untypable term (with type: HomNet * HomNet)

'(transitionsMap h2, transitionsMap h1)'

### Hint 114.59,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.59,

untypable term (with type: HomNet)

'h2'

### Hint 114.79,

in type of '(var h1 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.79,

untypable term (with type: HomNet)

'h1'

### Hint 114.86,

in type of '(var h2 : HomSys)'

typename 'gn_t1008' (93.8)

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

### Hint 114.86,

untypable term (with type: HomNet)

'h2'