Class FUNCTION-ALLOWED-IN-VT-CONSTRAINT

• Defined in theory: Vt-design
• Source code: vt-design.lisp

Slots on this class:

Documentation:

A function-constant is allowed in a VT constraint iff it is the name of a part-slot, a parameter-slot, or it is one of the operators allowed by VT.

Instance-Of: Class

Equivalence Axioms:

(<=> (Function-Allowed-In-Vt-Constraint ?Function-Constant)
     (Or (Subpart-Slot (Denotation ?Function-Constant))
         (Parameter-Slot (Denotation ?Function-Constant))
         (Member ?Function-Constant
                 (Setof '+
                        '-
                        '*
                        '/
                        'Setof
                        'Square
                        'Sqrt
                        'Floor
                        'Invsin))))

Axioms:

(Or (Subpart-Slot (Denotation ?Function-Constant))
    (Parameter-Slot (Denotation ?Function-Constant))
    (Member ?Function-Constant
            (Setof '+
                   '-
                   '*
                   '/
                   'Setof
                   'Square
                   'Sqrt
                   'Floor
                   'Invsin)))

Other Related Axioms:

(Restricted-Constraint-Sentence ?Sentence
                                (One-Of 'And
                                        'Or
                                        'Not
                                        '=>
                                        '<=
                                        '<=>)
                                (One-Of '=
                                        '/=
                                        '<
                                        '>
                                        '=<
                                        '>=
                                        'Member)
                                Function-Allowed-In-Vt-Constraint
                                Atomic-Term)

(=> (Vt-Constraint-Sentence ?Sentence)
    (Restricted-Constraint-Sentence ?Sentence
                                    (One-Of 'And
                                            'Or
                                            'Not
                                            '=>
                                            '<=
                                            '<=>)
                                    (One-Of '=
                                            '/=
                                            '<
                                            '>
                                            '=<
                                            '>=
                                            'Member)
                                    Function-Allowed-In-Vt-Constraint
                                    Atomic-Term))

(<=> (Function-Allowed-In-Vt-Constraint ?Function-Constant)
     (Or (Subpart-Slot (Denotation ?Function-Constant))
         (Parameter-Slot (Denotation ?Function-Constant))
         (Member ?Function-Constant
                 (Setof '+
                        '-
                        '*
                        '/
                        'Setof
                        'Square
                        'Sqrt
                        'Floor
                        'Invsin))))