2764758795be1dc0979461bf966e450c10e776f2Christian Maederlibrary S

2764758795be1dc0979461bf966e450c10e776f2Christian Maeder

80731efb785166b88edda6c2077f14e2e2858c06cmaederspec S =

2764758795be1dc0979461bf966e450c10e776f2Christian Maeder

2764758795be1dc0979461bf966e450c10e776f2Christian Maederfree type Bool ::= True | False

2764758795be1dc0979461bf966e450c10e776f2Christian Maeder

2764758795be1dc0979461bf966e450c10e776f2Christian Maederfree type List ::= Nil | Cons(head :? Bool; tail :? List)

2764758795be1dc0979461bf966e450c10e776f2Christian Maeder

2764758795be1dc0979461bf966e450c10e776f2Christian Maederwith Bool |-> bool, True |-> true', False |-> false',

2764758795be1dc0979461bf966e450c10e776f2Christian Maeder List |-> list, Nil |-> nil, Cons |-> cons, head |-> Head,

80731efb785166b88edda6c2077f14e2e2858c06cmaeder tail |-> Tail

80731efb785166b88edda6c2077f14e2e2858c06cmaeder

80731efb785166b88edda6c2077f14e2e2858c06cmaeder

80731efb785166b88edda6c2077f14e2e2858c06cmaederspec T =

80731efb785166b88edda6c2077f14e2e2858c06cmaeder

80731efb785166b88edda6c2077f14e2e2858c06cmaederfree type bool ::= false' | true';

80731efb785166b88edda6c2077f14e2e2858c06cmaeder list ::= cons(Head :? bool; Tail :? list) | nil

80731efb785166b88edda6c2077f14e2e2858c06cmaeder

80731efb785166b88edda6c2077f14e2e2858c06cmaederview v : S to T