gistfile1.txt

(declare-datatypes () (
  (Ty (base (idx Int)) 
      (arrow (src Ty) (tar Ty))
      (prod (c1 Ty) (c2 Ty)) 
      )))
      
 (declare-datatypes () (
   (Expr exprA
         exprAtoBtoC
         exprB
         exprAtoCtoD
         (ap (ap1 Expr) (ap2 Expr))
   )
 ))

(declare-fun hastype (Expr Ty) Bool)
(assert (forall ((a Expr) (b Expr) (t1 Ty) (t2 Ty)) 
  (=> (and (hastype a (arrow t1 t2)) (hastype b t1))
      (hastype (ap a b) t2))))

(define-fun A () Ty (base 0))
(define-fun B () Ty (base 1))
(define-fun C () Ty (base 2))
(define-fun D () Ty (base 3))

(assert (hastype exprAtoBtoC (arrow A (arrow B C))))
(assert (hastype exprA A))
(assert (hastype exprB B))
(assert (hastype exprAtoCtoD (arrow A (arrow C D))))

(define-fun is-appl ((a Expr) (t Ty)) Bool
  (exists ((s Ty) (f Expr) (b Expr)) 
    (and (hastype f (arrow s t))
         (hastype b s)
         (= a (ap f b))
    )
  )
)
(define-fun disjointness ((e Expr) (t Ty)) Bool
  (forall ((e1 Expr))
    (=> (hastype e1 t)
      (or (= e1 e) (is-appl e1 t))
    )
  )
)
(assert (disjointness exprA A))
(assert (disjointness exprB B))
(assert (disjointness exprAtoBtoC (arrow A (arrow B C))))
(assert (disjointness exprAtoCtoD (arrow A (arrow C D))))

(assert (forall ((a Expr) (t1 Ty) (t2 Ty))
  (=> (and (hastype a t1) (hastype a t2)) (= t1 t2))
))

(declare-const z Expr)
(assert (hastype z D))

(check-sat)
(get-model)