KB Mapping

Methods for mapping over the KB datastructures. The WITH- macros also provide relevant mts for most functions in which the microtheory is an optional argument. 

macro WITH-MT : (mt &body body)
MT and all its genl mts are relevant within BODY. 

macro WITH-ALL-MTS : (&body body)
All mts are relevant within BODY. 

macro WITH-JUST-MT : (mt &body body)
Only MT is relevant within BODY (no genl mts). 

macro WITH-MT-LIST : (mt-list &body body)
Each mt in the list MT-LIST is relevant within BODY (no genl mts). 

macro WITH-ANY-MT : (&body body)
Any mt can be used for relevance for a particular inference within &BODY. 

macro WITH-GENL-MTS : (mt &body body)
MT and all its genl mts are relevant within BODY. 

macro MAP-MTS : ((var) &body body)
Iterate over all microtheories, binding VAR to an mt and executing BODY. 

function MAP-TERM : (function term)
Apply FUNCTION to each assertion indexed from TERM.
FUNCTION must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function MAP-TERM-SELECTIVE : (function term test &optional truth)
Apply FUNCTION to each assertion indexed from TERM with TRUTH that passes TEST.
If TRUTH is nil, all assertions are mapped.
FUNCTION must satisfy FUNCTION-SPEC-P.
TEST must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function MAP-TERM-GAFS : (function term &optional truth)
Apply FUNCTION to every gaf indexed from TERM.
If TRUTH is nil, all assertions are mapped.
FUNCTION must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function MAP-MT-CONTENTS : (function term &optional truth gafs-only)
Apply FUNCTION to each assertion with TRUTH in MT TERM.
If TRUTH is nil, all assertions are mapped.
If GAFS-ONLY, then only gafs are mapped.
FUNCTION must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function MAP-MT-INDEX : (function mt &optional truth gafs-only)
Apply FUNCTION to each assertion with TRUTH at mt index MT.
If TRUTH is nil, all assertions are mapped.
If GAFS-ONLY, then only gafs are mapped.
FUNCTION must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function MAP-OTHER-INDEX : (function term &optional truth gafs-only)
Apply FUNCTION to each assertion with TRUTH at other index TERM.
If TRUTH is nil, all assertions are mapped.
If GAFS-ONLY, then only gafs are mapped.
FUNCTION must satisfy FUNCTION-SPEC-P.
Single value returned satisfies NULL. 

function GATHER-INDEX : (term &optional remove-duplicates?)
Return a list of all mt-relevant assertions indexed via TERM.
If REMOVE-DUPLICATES? is non-nil, assertions are guaranteed to only be listed once.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-INDEX-IN-ANY-MT : (term &optional remove-duplicates?)
Return a list of all assertions indexed via TERM.
If REMOVE-DUPLICATES? is non-nil, assertions are guaranteed to only be listed once.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-EXCEPTION-RULE-INDEX : (rule &optional mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) it has a positive literal of the form (abnormal <whatever> RULE)
b) if MT is non-nil, then MT must be its microtheory
c) if DIRECTION is non-nil, then DIRECTION must be its direction.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-FUNCTION-EXTENT-INDEX : (func)
Return a list of all #$termOfUnit assertions such that:
FUNC is the functor of the naut arg2.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-FUNCTION-RULE-INDEX : (func &optional mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) it has a negative literal of the form (termOfUnit <whatever> (FUNC . <whatever>))
b) if MT is non-nil, then MT must be its microtheory
c) if DIRECTION is non-nil, then DIRECTION must be its direction.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-GAF-ARG-INDEX : (term argnum &optional pred mt truth)
Return a list of all gaf assertions such that:
a) TERM is its ARGNUMth argument
b) if TRUTH is non-nil, then TRUTH is its truth value
c) if PRED is non-nil, then PRED must be its predicate
d) if MT is non-nil, then MT must be its microtheory (and PRED must be non-nil).
ARGNUM must satisfy POSITIVE-INTEGER-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-GENL-MT-RULE-INDEX : (genl-mt sense &optional rule-mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) if SENSE is :pos, it has a positive literal of the form (genlMt <whatever> GENL-MT)
b) if SENSE is :neg, it has a negative literal of the form (genlMt <whatever> GENL-MT)
c) if RULE-MT is non-nil, then RULE-MT must be its microtheory
d) if DIRECTION is non-nil, then DIRECTION must be its direction.
SENSE must satisfy SENSE-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-GENLS-RULE-INDEX : (collection sense &optional mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) if SENSE is :pos, it has a positive literal of the form (genls <whatever> COLLECTION)
b) if SENSE is :neg, it has a negative literal of the form (genls <whatever> COLLECTION)
c) if MT is non-nil, then MT must be its microtheory
d) if DIRECTION is non-nil, then DIRECTION must be its direction.
SENSE must satisfy SENSE-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-ISA-RULE-INDEX : (collection sense &optional mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) if SENSE is :pos, it has a positive literal of the form (isa <whatever> COLLECTION)
b) if SENSE is :neg, it has a negative literal of the form (isa <whatever> COLLECTION)
c) if MT is non-nil, then MT must be its microtheory
d) if DIRECTION is non-nil, then DIRECTION must be its direction.
SENSE must satisfy SENSE-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-MT-INDEX : (term)
Return a list of all assertions such that TERM is its microtheory.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-NART-ARG-INDEX : (term argnum &optional func)
Return a list of all #$termOfUnit assertions with a naut arg2 such that:
a) TERM is its ARGNUMth argument
b) if FUNC is non-nil, then FUNC must be its functor
ARGNUM must satisfy POSITIVE-INTEGER-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-OTHER-INDEX : (term)
Return a list of other assertions mentioning TERM but not indexed in any other more useful manner.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-PREDICATE-EXTENT-INDEX : (pred &optional mt truth)
Return a list of all gaf assertions such that:
a) PRED is its predicate
b) if TRUTH is non-nil, then TRUTH is its truth value
c) if MT is non-nil, then MT must be its microtheory.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-PREDICATE-RULE-INDEX : (pred sense &optional mt direction)
Return a list of all non-gaf assertions (rules) such that:
a) if SENSE is :pos, it has PRED as a predicate in a positive literal
b) if SENSE is :neg, it has PRED as a predicate in a negative literal
c) if MT is non-nil, then MT must be its microtheory
d) if DIRECTION is non-nil, then DIRECTION must be its direction.
SENSE must satisfy SENSE-P.
Single value returned is a list of elements satisfying ASSERTION-P. 

function GATHER-TERM-ASSERTIONS : (term &optional mt)
Return a list of all mt-relevant assertions of TERM.
Single value returned is a list of elements satisfying ASSERTION-P. 

function FPRED-VALUE : (term pred &optional index-arg gather-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return the term in the GATHER-ARG position if such an assertion exists.
Otherwise, return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies HL-TERM-P or is NIL. 

function FPRED-VALUE-IN-MT : (term pred mt &optional index-arg gather-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return the term in the GATHER-ARG position if such an assertion exists.
Otherwise, return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MT must satisfy HLMT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies HL-TERM-P or is NIL. 

function FPRED-VALUE-IN-MTS : (term pred mts &optional index-arg gather-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return the term in the GATHER-ARG position if such an assertion exists.
Otherwise, return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MTS must satisfy LISTP.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies HL-TERM-P or is NIL. 

function FPRED-VALUE-IN-ANY-MT : (term pred &optional index-arg gather-arg truth)
Find the first gaf assertion such that:
(a) the assertion is allowed to be in any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return the term in the GATHER-ARG position if such an assertion exists.
Otherwise, return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies HL-TERM-P or is NIL. 

function FPRED-VALUE-IN-RELEVANT-MTS : (term pred &optional mt index-arg gather-arg truth)
If MT is NIL, behaves like FPRED-VALUE. Otherwise, behaves like FPRED-VALUE-IN-MT.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies HL-TERM-P or is NIL. 

function PRED-VALUES : (term pred &optional index-arg gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of the terms in the GATHER-ARG position of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-VALUES-IN-MT : (term pred mt &optional index-arg gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of the terms in the GATHER-ARG position of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MT must satisfy HLMT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-VALUES-IN-MTS : (term pred mts &optional index-arg gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of the terms in the GATHER-ARG position of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MTS must satisfy LISTP.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-VALUES-IN-ANY-MT : (term pred &optional index-arg gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is allowed to be in any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of the terms in the GATHER-ARG position of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-VALUES-IN-RELEVANT-MTS : (term pred &optional mt index-arg gather-arg truth)
If MT is NIL, behaves like PRED-VALUES. Otherwise, behaves like PRED-VALUES-IN-MT
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-REFS : (pred &optional gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
Return a list of the terms in the GATHER-ARG position of all such assertions.
PRED must satisfy FORT-P.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-REFS-IN-MT : (pred mt &optional gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
Return a list of the terms in the GATHER-ARG position of all such assertions.
PRED must satisfy FORT-P.
MT must satisfy HLMT-P.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-REFS-IN-MTS : (pred mts &optional gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
Return a list of the terms in the GATHER-ARG position of all such assertions.
PRED must satisfy FORT-P.
MTS must satisfy LISTP.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-REFS-IN-ANY-MT : (pred &optional gather-arg truth)
Find all gaf assertions such that:
(a) the assertion is allowed to be in any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
Return a list of the terms in the GATHER-ARG position of all such assertions.
PRED must satisfy FORT-P.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function PRED-REFS-IN-RELEVANT-MTS : (pred &optional mt gather-arg truth)
If MT is NIL, behaves like PRED-REFS. Otherwise, behaves like PRED-REFS-IN-MT
PRED must satisfy FORT-P.
GATHER-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying HL-TERM-P. 

function SOME-PRED-VALUE : (term pred &optional index-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return T if such an assertion exists, otherwise return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function SOME-PRED-VALUE-IN-MT : (term pred mt &optional index-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return T if such an assertion exists, otherwise return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MT must satisfy HLMT-P.
INDEX-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function SOME-PRED-VALUE-IN-MTS : (term pred mts &optional index-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return T if such an assertion exists, otherwise return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
MTS must satisfy LISTP.
INDEX-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function SOME-PRED-VALUE-IN-ANY-MT : (term pred &optional index-arg truth)
Find the first gaf assertion such that:
(a) the assertion is allowed to be in any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return T if such an assertion exists, otherwise return NIL.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function SOME-PRED-VALUE-IN-RELEVANT-MTS : (term pred &optional mt index-arg truth)
If MT is NIL, behaves like SOME-PRED-VALUE. Otherwise, behaves like SOME-PRED-VALUE-IN-MT
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-U-V-HOLDS : (pred u v &optional u-arg v-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) U is the term in the U-ARG position.
(e) V is the term in the V-ARG position.
Return T if such an assertion exists, otherwise return NIL.
PRED must satisfy FORT-P.
U must satisfy INDEXED-TERM-P.
V must satisfy HL-TERM-P.
U-ARG must satisfy INTEGERP.
V-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-U-V-HOLDS-IN-MT : (pred u v mt &optional u-arg v-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) U is the term in the U-ARG position.
(e) V is the term in the V-ARG position.
Return T if such an assertion exists, otherwise return NIL.
PRED must satisfy FORT-P.
U must satisfy INDEXED-TERM-P.
V must satisfy HL-TERM-P.
MT must satisfy HLMT-P.
U-ARG must satisfy INTEGERP.
V-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-U-V-HOLDS-IN-MTS : (pred u v mts &optional u-arg v-arg truth)
Find the first gaf assertion such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) U is the term in the U-ARG position.
(e) V is the term in the V-ARG position.
Return T if such an assertion exists, otherwise return NIL.
PRED must satisfy FORT-P.
U must satisfy INDEXED-TERM-P.
V must satisfy HL-TERM-P.
MTS must satisfy LISTP.
U-ARG must satisfy INTEGERP.
V-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-U-V-HOLDS-IN-ANY-MT : (pred u v &optional u-arg v-arg truth)
Find the first gaf assertion such that:
(a) the assertion is allowed to be in any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) U is the term in the U-ARG position.
(e) V is the term in the V-ARG position.
Return T if such an assertion exists, otherwise return NIL.
PRED must satisfy FORT-P.
U must satisfy INDEXED-TERM-P.
V must satisfy HL-TERM-P.
U-ARG must satisfy INTEGERP.
V-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-U-V-HOLDS-IN-RELEVANT-MTS : (pred u v &optional mt u-arg v-arg truth)
If MT is NIL, behaves like PRED-U-V-HOLDS. Otherwise, behaves like PRED-U-V-HOLDS-IN-MT
PRED must satisfy FORT-P.
U must satisfy INDEXED-TERM-P.
V must satisfy HL-TERM-P.
U-ARG must satisfy INTEGERP.
V-ARG must satisfy INTEGERP.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies BOOLEANP. 

function PRED-VALUE-TUPLES : (term pred index-arg gather-args &optional truth)
Find all gaf assertions such that:
(a) the assertion is in a relevant microtheory (relevance is established outside)
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARGS must satisfy LISTP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying LISTP. 

function PRED-VALUE-TUPLES-IN-MT : (term pred index-arg gather-args mt &optional truth)
Find all gaf assertions such that:
(a) the assertion is microtheory MT
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARGS must satisfy LISTP.
MT must satisfy HLMT-P.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying LISTP. 

function PRED-VALUE-TUPLES-IN-MTS : (term pred index-arg gather-args mts &optional truth)
Find all gaf assertions such that:
(a) the assertion is in one of the microtheories in the list MTS
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARGS must satisfy LISTP.
MTS must satisfy LISTP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying LISTP. 

function PRED-VALUE-TUPLES-IN-ANY-MT : (term pred index-arg gather-args &optional truth)
Find all gaf assertions such that:
(a) the assertion is allowed to be from any microtheory
(b) if TRUTH is non-nil, the assertion has TRUTH as its truth value
(c) PRED is the predicate used.
(d) TERM is the term in the INDEX-ARG position.
Return a list of tuples formed from the GATHER-ARGS positions of all such assertions.
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARGS must satisfy LISTP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying LISTP. 

function PRED-VALUE-TUPLES-IN-RELEVANT-MTS : (term pred index-arg gather-args &optional mt truth)
If MT is NIL, behaves like PRED-VALUE-TUPLES. Otherwise, behaves like PRED-VALUE-TUPLES-IN-MT
TERM must satisfy INDEXED-TERM-P.
PRED must satisfy FORT-P.
INDEX-ARG must satisfy INTEGERP.
GATHER-ARGS must satisfy LISTP.
TRUTH must satisfy TRUTH-P.
Single value returned is a list of elements satisfying LISTP.