Nuprl Definition : wf-bound-terms
wf-bound-terms(opr;sort;arity;f) ==
{bts:(varname() List × wfterm(opr;sort;arity)) List|
(||bts|| = ||arity f|| ∈ ℤ)
∧ (∀i:ℕ||bts||. ((||fst(bts[i])|| = (fst(arity f[i])) ∈ ℤ) ∧ ((sort (snd(bts[i]))) = (snd(arity f[i])) ∈ ℤ)))}
Definitions occuring in Statement :
wfterm: wfterm(opr;sort;arity),
varname: varname(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
product: x:A × B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
list: T List,
wfterm: wfterm(opr;sort;arity),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
and: P ∧ Q,
length: ||as||,
pi1: fst(t),
equal: s = t ∈ T,
int: ℤ,
pi2: snd(t),
select: L[n],
apply: f a
FDL editor aliases :
wf-bound-terms
Latex:
wf-bound-terms(opr;sort;arity;f) ==
\{bts:(varname() List \mtimes{} wfterm(opr;sort;arity)) List|
(||bts|| = ||arity f||)
\mwedge{} (\mforall{}i:\mBbbN{}||bts||
((||fst(bts[i])|| = (fst(arity f[i]))) \mwedge{} ((sort (snd(bts[i]))) = (snd(arity f[i])))))\}
Date html generated:
2020_05_19-PM-09_58_30
Last ObjectModification:
2020_03_09-PM-04_10_19
Theory : terms
Home
Index