Lines Matching defs:fm
618 ``���a. ~(a ��� supp (fm_pmact string_pmact ^t_pmact_t) fm)``,
619 Q_TAC (NEW_TAC "z") `supp (fm_pmact string_pmact ^t_pmact_t) fm` THEN
623 ``~(x ��� supp (set_pmact ^t_pmact_t) (FRANGE fm)) =
624 ���y. y ��� FDOM fm ==> ~(x ��� FV (fm ' y))``,
630 val fm = mk_exists(v,concl c1)
632 CHOOSE (v, thm) (EXISTS(fm,v) c1)
642 ``���fm. FINITE (supp (set_pmact ^t_pmact_t) (FRANGE fm))``,
659 |> Q.INST [`vr` |-> `\s fm. if s ��� FDOM fm then fm ' s else VAR s`,
660 `lm` |-> `\r v t fm. LAM v (r fm)`, `apm` |-> `^t_pmact_t`,
662 `ap` |-> `\r1 r2 t1 t2 fm. r1 fm @@ r2 fm`,
669 |> CONV_RULE (DEPTH_CONV (rename_vars [("p", "fm")]))
689 ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
690 x ��� FDOM fm ���
691 ���y. y ��� FDOM fm ��� x ��� FV (fm ' y)``,
697 ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
698 x ��� FDOM fm ��� ���y. y ��� FDOM fm ==> x ��� FV (fm ' y)``,