453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervars a,b: Type

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedergenerated type Set a ::= empty | add a (Set a)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedergenerated type Sys b ::= node b (Set (Sys b))

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedertype Nat

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedervar a: Type

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maedergenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type L ::= abs (L -> L)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type Tree a b ::= leaf b | branch (a -> Tree a b)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

20921b0900acb7e19a778e4b309a7e6d6c305e5eChristian Maederfree type List a ::= nil | cons (a; List a)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maedervar b : Type

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maederop map : (a -> b) -> List a -> List b

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maeder

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederfree type Tree a b ::= leaf a | branch (b -> List (Tree a b))

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervar c : Type

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maederop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maederop __ o __ : (b -> c) * (a -> b) -> a -> c

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maeder

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maedervars f : a -> c; g : (b -> List c) -> c; x : a; s : b -> List (Tree a b)

453c9b0df0380abe5abb38db3b15530bd3b3dcf5Christian Maeder. fold f g (leaf x) = f x

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder. def (fold f g (branch s))

4dd227b3f9c659b37083476347d01e2fdd0c71dbChristian Maeder. fold f g (branch s) = g (map (fold f g) o s)

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder

1256a6994be0c94373a47f8b30747727b24c27faChristian Maedervar Q : Pred(Set (Sys b)); P : Pred (Sys b)

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder. (forall x : b; s : Set (Sys b) . Q s => P (node x s))

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder /\ Q empty

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

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder => forall t : Sys b . P t

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder

1256a6994be0c94373a47f8b30747727b24c27faChristian Maedervar R : Pred(CTree a)

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder. (forall x : a . R (leaf x))

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder /\ (forall f : Nat ->? CTree a .

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

1256a6994be0c94373a47f8b30747727b24c27faChristian Maeder => forall t : CTree a . R t