Nuprl Definition : immediate-subterm
s < t ==
∃f:opr. ∃bts:bound-term(opr) List. ((t = mkterm(f;bts) ∈ term(opr)) ∧ (∃i:ℕ||bts||. (s = (snd(bts[i])) ∈ term(opr))))
Definitions occuring in Statement :
bound-term: bound-term(opr),
mkterm: mkterm(opr;bts),
term: term(opr),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
pi2: snd(t),
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
list: T List,
bound-term: bound-term(opr),
and: P ∧ Q,
mkterm: mkterm(opr;bts),
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
equal: s = t ∈ T,
term: term(opr),
pi2: snd(t),
select: L[n]
FDL editor aliases :
immediate-subterm
Latex:
s < t ==
\mexists{}f:opr. \mexists{}bts:bound-term(opr) List. ((t = mkterm(f;bts)) \mwedge{} (\mexists{}i:\mBbbN{}||bts||. (s = (snd(bts[i])))))
Date html generated:
2020_05_19-PM-09_54_03
Last ObjectModification:
2020_03_09-PM-04_08_29
Theory : terms
Home
Index