vars a, b : Type

generated type Set a ::= empty | add a (Set a)

generated type Sys b ::= node b (Set (Sys b))

type Nat

var a : Type

generated type CTree a ::= leaf a | branch (Nat ->? CTree a)

free type L ::= abs (L -> L)

free type Tree a b ::= leaf b | branch (a -> Tree a b)

free type List a ::= nil | cons (a; List a)

var b : Type

op map : (a -> b) -> List a -> List b

free type Tree a b ::= leaf a | branch (b -> List (Tree a b))

var c : Type

op fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

op __o__ : (b -> c) * (a -> b) -> a -> c

vars f : a -> c; g : (b -> List c) -> c; x : a;

s : b -> List (Tree a b)

. fold f g (leaf x) = f x

. def fold f g (branch s)

. fold f g (branch s) = g (map (fold f g) o s);

vars Q : Pred (Set (Sys b)); P : Pred (Sys b)

. ((forall x : b; s : Set (Sys b) . Q s => P (node x s)) /\ Q ""

/\ forall s : Set (Sys b); t : Sys b . Q s /\ P t => Q (add t s))

=> forall t : Sys b . P t;

var R : Pred (CTree a)

. ((forall x : a . R (leaf x))

/\ forall f : Nat ->? CTree a

. (forall x : Nat . def f x => R (f x)) => R (branch f))

=> forall t : CTree a . R t;

types

CTree : Type -> Type;

L : Type;

List : Type -> Type;

Nat : Type;

Set : Type -> Type;

Sys : Type -> Type;

Tree : Type -> Type -> Type

vars

a : Type %(var_5)%;

b : Type %(var_10)%;

c : Type %(var_13)%

op __o__ : forall a : Type; b : Type; c : Type

. (b -> c) * (a -> b) -> a -> c

op abs : (L -> L) -> L %(constructor)%

op add : forall a : Type . a -> Set a -> Set a %(constructor)%

op branch : forall a : Type . (Nat ->? CTree a) -> CTree a

%(constructor)%

op branch : forall a : Type; b : Type

. (b -> List (Tree a b)) -> Tree a b

%(constructor)%

op branch : forall a : Type; b : Type . (a -> Tree a b) -> Tree a b

%(constructor)%

op cons : forall a : Type . a * List a -> List a %(constructor)%

op empty : forall a : Type . Set a %(constructor)%

op fold : forall a : Type; b : Type; c : Type

. (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

op leaf : forall a : Type . a -> CTree a %(constructor)%

op leaf : forall a : Type; b : Type . b -> Tree a b %(constructor)%

op leaf : forall a : Type; b : Type . a -> Tree a b %(constructor)%

op map : forall a : Type; b : Type . (a -> b) -> List a -> List b

op nil : forall a : Type . List a %(constructor)%

op node : forall b : Type . b -> Set (Sys b) -> Sys b

%(constructor)%

vars

P : Pred (Sys b);

Q : Pred (Set (Sys b));

R : Pred (CTree a);

f : a -> c;

g : (b -> List c) -> c;

s : b -> List (Tree a b);

x : a

generated type Set(a : Type) ::= add (a) (Set a) | empty %(ga_Set)%

generated type Sys(b : Type) ::= node (b) (Set (Sys b)) %(ga_Sys)%

generated type CTree(a : Type) ::=

branch (Nat ->? CTree a) | leaf (a) %(ga_CTree)%

free type L ::= abs (L -> L) %(ga_L)%

free type Tree(a : Type)(b : Type) ::=

branch (a -> Tree a b) | leaf (b) %(ga_Tree)%

free type List(a : Type) ::= cons (a; List a) | nil %(ga_List)%

free type Tree(a : Type)(b : Type) ::=

branch (b -> List (Tree a b)) | leaf (a) %(ga_Tree)%

forall

a : Type; b : Type; c : Type; f : a -> c; g : (b -> List c) -> c;

x : a

. fold f g

((op leaf : forall a : Type; b : Type . a -> Tree a b) x)

= f x

forall

a : Type; b : Type; c : Type; f : a -> c; g : (b -> List c) -> c;

s : b -> List (Tree a b)

. def fold f g

((op branch :

forall a : Type; b : Type . (b -> List (Tree a b)) -> Tree a b)

s)

forall

a : Type; b : Type; c : Type; f : a -> c; g : (b -> List c) -> c;

s : b -> List (Tree a b)

. fold f g

((op branch :

forall a : Type; b : Type . (b -> List (Tree a b)) -> Tree a b)

s)

= g (map (fold f g) o s)

forall b : Type; P : Pred (Sys b); Q : Pred (Set (Sys b))

. ((forall x : b; s : Set (Sys b) . Q s => P (node x s)) /\ Q ""

/\ forall s : Set (Sys b); t : Sys b . Q s /\ P t => Q (add t s))

=> forall t : Sys b . P t

forall a : Type; R : Pred (CTree a)

. ((forall x : a

. R ((op leaf : forall a : Type . a -> CTree a) x))

/\ forall f : Nat ->? CTree a

. (forall x : Nat . def f x => R (f x))

=> R

((op branch : forall a : Type . (Nat ->? CTree a) -> CTree a) f))

=> forall t : CTree a . R t

1.6: ### Hint: is type variable 'a'

1.8: ### Hint: is type variable 'b'

6.5: ### Hint: is type variable 'a'

6.5: ### Hint: rebound type variable 'a'

9.22: *** Error: negative datatype occurrence of 'L'

15.5: ### Hint: is type variable 'b'

15.5: ### Hint: rebound type variable 'b'

18.11-18.14: ### Hint: redeclared type 'Tree'

20.5: ### Hint: is type variable 'c'

23.15-23.20: ### Hint:

no kind found for 'b -> c'

expected: {Cpo}

found: {Type}

23.15-23.20: ### Hint:

no kind found for 'b -> c'

expected: {Cppo}

found: {Type}

25.8: ### Hint: not a class 'a'

25.8: ### Hint: not a class 'c'

25.20: ### Hint: not a kind '(b -> List c) -> c'

25.44: ### Hint: not a class 'a'

25.51: ### Hint: not a kind 'b -> List (Tree a b)'

26.13-26.18: ### Hint:

in type of '(op leaf : forall a : Type . a -> CTree a) (var x : a)'

typename 'CTree' (7.20)

is not unifiable with type 'Tree _v15_a' (21.50)

26.3-26.18: ### Hint:

unable to prove: b < a of '(((op fold :

forall a : Type; b : Type; c : Type

. (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c)

(var f : a -> c))

(var g : (b -> List c) -> c))

((op leaf : forall a : Type; b : Type . b -> Tree a b) (var x : a))'

27.25: ### Hint:

rejected 'List < CTree' of '(var s : b -> List (Tree a b))'

27.25: ### Hint:

rejected 'Nat < b' of '(var s : b -> List (Tree a b))'

27.25: ### Hint:

untypeable term (with type: Nat ->? CTree _v27_a) 's'

27.25: ### Hint:

in type of '(var s : b -> List (Tree a b))'

typename 'List' (25.61)

is not unifiable with type 'Tree b' (25.53)

27.25: ### Hint:

untypeable term (with type: _v30_a -> Tree _v30_a _v31_b) 's'

28.20: ### Hint:

rejected 'List < CTree' of '(var s : b -> List (Tree a b))'

28.20: ### Hint:

rejected 'Nat < b' of '(var s : b -> List (Tree a b))'

28.20: ### Hint:

untypeable term (with type: Nat ->? CTree _v39_a) 's'

28.20: ### Hint:

in type of '(var s : b -> List (Tree a b))'

typename 'List' (25.61)

is not unifiable with type 'Tree b' (25.53)

28.20: ### Hint:

untypeable term (with type: _v42_a -> Tree _v42_a _v43_b) 's'

30.7: ### Hint: not a kind 'Pred (Set (Sys b))'

30.30: ### Hint: not a kind 'Pred (Sys b)'

32.13: ### Hint: not a class 'b'

32.20: ### Hint: not a kind 'Set (Sys b)'

34.16: ### Hint: not a kind 'Set (Sys b)'

34.33: ### Hint: not a kind 'Sys b'

35.15: ### Hint: not a kind 'Sys b'

32.11: ### Hint: rebound variable 'x'

32.18: ### Hint: rebound variable 's'

34.14: ### Hint: rebound variable 's'

37.7: ### Hint: not a kind 'Pred (CTree a)'

38.13: ### Hint: not a class 'a'

39.16: ### Hint: not a kind 'Nat ->? CTree a'

40.15: ### Hint: not a class 'Nat'

41.15: ### Hint: not a kind 'CTree a'

38.11: ### Hint: rebound variable 'x'

38.22-38.27: ### Hint:

in type of '(op leaf : forall a : Type; b : Type . b -> Tree a b) (var x : a)'

typename 'CTree' (37.18)

is not unifiable with type 'Tree _v73_a' (11.16)

38.22-38.27: ### Hint:

in type of '(op leaf : forall a : Type; b : Type . a -> Tree a b) (var x : a)'

typename 'CTree' (37.18)

is not unifiable with type 'Tree a' (38.15)

39.14: ### Hint: rebound variable 'f'

40.13: ### Hint: rebound variable 'x'

40.56: ### Hint:

in type of '(var f : Nat ->? CTree a)'

typename 'a' (39.32)

is not unifiable with type 'Tree _v81_a Nat' (39.20)

40.56: ### Hint:

untypeable term (with type: _v80_b -> List (Tree _v81_a _v80_b))

'f'

40.56: ### Hint:

in type of '(var f : Nat ->? CTree a)'

typename 'CTree' (39.30)

is not unifiable with type 'Tree Nat' (39.20)

40.56: ### Hint:

untypeable term (with type: _v82_a -> Tree _v82_a _v83_b) 'f'