; Deps: smt.plf th_base.plf
(declare forall (! s sort
                   (! t (term s)
                      (! f formula
                         formula))))

;This program recursively checks the instantiation.
;Composite terms (such as "apply _ _ ...") are handled recursively.
;Then, if ti and t are equal, we return true. Otherwise, we first verify that t is the variable for which ti is substitued (ifmarked). if this is the case, ti should be equal to k.

(program is_inst_t ((ti term) (t term) (k term)) bool
         (match t
                ((apply s1 s2 t1 t2)
                 (match ti
                        ((apply si1 si2 ti1 ti2)
                         (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
                        (default ff)))
                (default (ifequal ti t tt (ifmarked t (ifequal ti k tt ff) ff)))))


(program is_inst_f ((fi formula) (f formula) (k term)) bool
         (match f
                ((and f1 f2) (match fi
                                    ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
                                    (default ff)))
                ((or f1 f2) (match fi
                                   ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
                                   (default ff)))
                ((impl f1 f2) (match fi
                                     ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
                                     (default ff)))
                ((not f1) (match fi
                                 ((not fi1) (is_inst_f fi1 f1 k))
                                 (default ff)))
                ((iff f1 f2) (match fi
                                    ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
                                    (default ff)))
                ((xor f1 f2) (match fi
                                    ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
                                    (default ff)))
                ((ifte f1 f2 f3) (match fi
                                        ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k)
                                                                   (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff)))
                                                                   (ff ff)))
                                        (default ff)))
                ((= s t1 t2) (match fi
                                    ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
                                    (default ff)))
                ((forall s t1 f1) (match fi
                                         ((forall s ti1 fi1) (is_inst_f fi1 f1 k))
                                         (default ff)))
                (default ff)))

(program is_inst ((fi formula) (f formula) (t term) (k term)) bool
         (do (markvar t)
           (let f1 (is_inst_f fi f k)
             (do (markvar t) f1))))

(declare skolem
         (! s sort
            (! t (term s)
               (! f formula
                  (! p (th_holds (not (forall s t f)))
                     (! u (! k (term s)
                             (! fi formula
                                (! p1 (th_holds (not fi))
                                   (! r (^ (is_inst fi f t k) tt)
                                      (holds cln)))))
                        (holds cln)))))))

(declare inst
         (! s sort
            (! t (term s)
               (! f formula
                  (! k (term s)
                     (! fi formula
                        (! p (th_holds (forall s t f))
                           (! r (^ (is_inst fi f t k) tt)
                              (! u (! p1 (th_holds fi)
                                      (holds cln))
                                 (holds cln))))))))))