\section{Case study: simple typing in Mini-ML}

We offer the derivation of $\neg of$ as an example which 
combines the transformation technique for non-horn programs with 
extensional quantification. First we present the manually written 
code.

\begin{verbatim}

% exp: type.
tp : type.
nat: tp.
=> : tp -> tp -> tp. %infix  right 10 =>.
z : exp.
s: exp -> exp.
case : exp -> exp ->(exp -> exp) -> exp.
lamt : tp -> (exp -> exp) -> exp.
% lam :  (exp -> exp) -> exp.
app : exp -> exp -> exp.
appt : exp -> exp -> tp  -> exp.

of : exp -> tp -> type.

of_z : of z nat.
of_s : of (s E) nat <- of E nat.
of_case : of (case E1 E2 E3) T
	   <- of E1 nat
	   <- of E2 T
	   <- ({x:exp} of x nat -> of (E3 x) T).

of_lamt : of (lamt T E) (T => T')
	   <- ({x:exp} of x T -> of (E x) T').
of_app : of (app E1 E2) T1
	  <- of E1 (T2 => T1)
	  <- of E2 T2.

nof : exp -> tp -> type.
diff : tp -> tp -> type.
ill : exp -> type. % ill E  iff  forall T. nof E T.

% no ill_z
ill_s1 : ill (s E) <- ill E.
ill_s2 : ill (s E) <- nof E nat.
% skipping ill_case

ill_app1 : ill (app E1 E2) <- ill E1.
ill_app2 : ill (app E1 E2) <- ill E2.
ill_app3 : ill (app E1 E2)
	    <- of E1 (T2 => T1)
	    <- nof E2 T2.
ill_app4 : ill (app E1 E2)
	    <- of E1 nat.

ill_lam : ill (lamt T E)
	   <- ({x:exp} ({T3:tp} nof x T3 <- diff T3 T)
		 -> of x T
		    % no ill x
		 -> ill (E x)).

% nats
n_z : nof z (T1 => T2).
n_s : nof (s E) (T1 => T2).
n_sr : nof  (s E) nat <- nof E nat.
nc1 : nof (case E1 E2 E3) T <- nof E1 nat.
nc2 : nof (case E1 E2 E3) T <- nof E2 T.
nc3 : nof (case E1 E2 E3) T
       <- ({x:exp}
	     ({T3:tp} nof x T3 <- diff T3 nat)
	     -> of x nat
	     -> nof (E3 x) T).

% functions

nap1a : nof (app E1 E2) T1 <- ill E1.
nap1b : nof (app E1 E2) T1 <- of E1 nat.
nap1c : nof (app E1 E2) T1 <- of E1 (T2 => T1') <- diff T1 T1'.
nap2 : nof (app E1 E2) T1 <- of E1 (T2 => T1) <- nof E2 T2.

lmt1 : nof (lamt T E) nat.
lmt2 : nof (lamt T E) (T1 => T2)
	<- diff T T1.
lmt3 : nof (lamt T E) (T => T2)
	<- ({x : exp}
	      ({T3:tp} (nof x T3) <- (diff T3 T))
	      -> of x T
	      -> (nof (E x) T2)).

d1: diff nat  (T1 => T2).
d2: diff  (T1 => T2) nat.
d3a: diff (T1 => T2) (T1' => T2') <- diff T1 T1'.
d3b: diff (T1 => T2) (T1' => T2') <- diff T2 T2'. 
\end{verbatim}

To be completed