%{
%query 1 * check shiftl (bit => bit & pos => pos).

%query 0 * check shiftl (nat => nat).

%query 1 * check inc (nat => pos).

%query 0 * check inc (nat => nat).

%query 1 * nat => pos <| nat => nat.
%query 1 * synth (inc # nat => pos) A.

%query 1 * check std (bit => nat).
%query 1 * check test1 pos.
%query 0 * check test2 nat.
%query 1 *
check plus (bit => bit => bit).

% Too many solutions?
%query * 2
D : check plus (nat => nat => nat &
	    nat => pos => pos &
	    pos => nat => pos &
	    pos => pos => pos).

%query 4 *
check (lam [plus] app (app plus (e 1)) (e 1))
           ((nat => nat => nat &
	       nat => pos => pos &
	       pos => nat => pos &
	       pos => pos => pos) => bit).

%query 1 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat).

%query 1 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => pos => pos).

%query 4 *
check (lam [plus] app (app plus (e 1)) (e 1))
(((nat => nat => nat)
    & (nat => pos => pos)
    & (pos => nat => pos)
    & (pos => pos => pos)) => nat).

%query 2 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat
	      & nat => pos => pos).

%query 12 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat       % *3 (3 ways to prove nat)
	      & nat => pos => pos   % *2 (2 ways to prove pos)
	      & pos => nat => pos). % *2 (2 ways to prove pos)

%query 108 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat		% *4 ways to prove nat
	      & nat => pos => pos	% *3 ways to prove pos
	      & pos => nat => pos	% *3 ways to prove pos
	      & pos => pos => pos).	% *3 ways to prove pos

%query 4 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat
	      & nat => nat => nat).

%query 108 *
check (fix [plus] lam [x] lam [y] app (app plus (e 1)) (e 1))
           (nat => nat => nat &
	       nat => pos => pos &
	       pos => nat => pos &
	       pos => pos => pos).

%query 1 *
synth ((fix [inc] lam [n]
	case n
	(e 1)
	([x] x 1)
	([x] (app inc x) 0)) # nat => pos)
A.

%query 1 *
check (fix [plus] lam [n] lam [m]
	 (case n m ([x] x 1) ([y] y 1)))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

%query 1 *
check (fix [plus] lam [n] lam [m]
	 (case n
	    m 
	    ([x] case m (x 0) ([y] y 1) ([y] y 1))
	    ([x] x 1)))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

%query 1 *
check (fix [plus] lam [n] lam [m]
	 (case n
	    m 
	    ([x] case m
	       (x 0)
	       ([y] y 1)
	       ([y] y 1))
	    ([x] case m
	       (x 1)
	       ([y] y 1)
	       ([y] y 1))))
(nat => nat => nat &
   nat => pos => pos &
   pos => nat => pos &
   pos => pos => pos).

}%
%query 20736 *
check plus' (nat => nat => nat &
	     nat => pos => pos &
	     pos => nat => pos &
	     pos => pos => pos).