e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maedersort s, t;

e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maederop snd : s * t -> t;

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederprogram snd (x, y) = y;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram snd (x, y) = y;

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederprogram snd (x, y) = y : t;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram snd (x, y) : t = y;

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederprogram snd (x, y) : t = y;

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maederprogram snd (x : s, y : t) : t = y;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiop a : s;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram b : s = a;

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederop b : s;

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederprogram b : s = a;

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowskiop x : s;

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder y : t;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiop c : t = snd (x : s, y : t);

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%% Type Constructors -----------------------------------------------------

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeders : Type

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedert : Type

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder%% Assumptions -----------------------------------------------------------

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskia : s %(op)%

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederb : s %(op)%

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederc : t %(op)% = (op snd : s * t -> t) ((op x : s), (op y : t)) as t

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskisnd : s * t -> t %(op)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskix : s %(op)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiy : t %(op)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%% Sentences -------------------------------------------------------------

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) : t

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %(pe_snd)%

cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederprogram snd ((var x : s) : s, (var y : t) : t) : t = (var y : t)

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder %(pe_snd)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram (var b : s) : s = a %(pe_b)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiprogram b = a %(pe_b)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskic = (snd (x, y) as t) %(def_c)%

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski%% Diagnostics -----------------------------------------------------------

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder*** Error 14.11-14.18, illegal toplevel pattern '((var x : s), (var y : s))'

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski### Warning 17.10, illegal lhs pattern '(var b : s)'

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder