type s, t

op snd : s * t -> t

program (op snd : s * t -> t) ((var x : s), (var y : t)) : t =

(var y : t)

program (op snd : s * t -> t) ((var x : s), (var y : t)) : t =

(var y : t)

program (op snd : s * t -> t) ((var x : s), (var y : t)) : t =

(var y : t) : t

program (op snd : s * t -> t) ((var x : s), (var y : t)) : t =

(var y : t)

program (op snd : s * t -> t) ((var x : s), (var y : t)) : t =

(var y : t)

program (op snd : s * t -> t) ((var x : s) : s, (var y : t) : t) :

t

= (var y : t)

op a : s

program (var b : s) : s = (op a : s)

op b : s

program (op b : s) = (op a : s)

op x : s;

y : t

op c : t = (op snd : s * t -> t) ((op x : s), (op y : t)) as t

%% Type Constructors -----------------------------------------------------

? : +Type -> Type

Logical : Type := ? Unit

Pred : -Type -> Type := \ a : -Type . a ->? Unit

Unit : Type

__*__ : +Type -> +Type -> Type

__*__*__ : +Type -> +Type -> +Type -> Type

__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

s : Type

t : Type

%% Assumptions -----------------------------------------------------------

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a * a ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

a : s %(op)%

b : s %(op)%

bottom : forall a : Type . a %(fun)%

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

def__ : forall a : Type . a ->? Unit %(fun)%

false : Unit %(fun)%

not__ : ? Unit ->? Unit %(fun)%

snd : s * t -> t %(op)%

true : Unit %(fun)%

x : s %(op)%

y : t %(op)%

�__ : ? Unit ->? Unit %(fun)%

%% Sentences -------------------------------------------------------------

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

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

program snd((var x : s), (var y : t)) : t = (var y : t) : t

%(pe_snd)%

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

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

program snd(((var x : s) : s), ((var y : t) : t)) : t =

(var y : t) %(pe_snd)%

program (var b : s) : s = a %(pe_b)%

program b = a %(pe_b)%

c = (snd(x, y) as t) %(def_c)%

%% Diagnostics -----------------------------------------------------------

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

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