Nuprl Definition : subterm-rel
subterm-rel(opr) == TC(λs,t. s < t)
Definitions occuring in Statement :
immediate-subterm: s < t,
term: term(opr),
transitive-closure: TC(R),
lambda: λx.A[x]
Definitions occuring in definition :
transitive-closure: TC(R),
term: term(opr),
lambda: λx.A[x],
immediate-subterm: s < t
FDL editor aliases :
subterm-rel
Latex:
subterm-rel(opr) == TC(\mlambda{}s,t. s < t)
Date html generated:
2020_05_19-PM-09_54_06
Last ObjectModification:
2020_03_09-PM-04_08_32
Theory : terms
Home
Index