Nuprl Definition : hereditarily
hereditarily(opr;s.P[s];t) == P[t] ∧ (∀s:term(opr). (s << t ⇒ P[s]))
Definitions occuring in Statement :
subterm: s << t,
term: term(opr),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
term: term(opr),
implies: P ⇒ Q,
subterm: s << t
FDL editor aliases :
hereditarily
Latex:
hereditarily(opr;s.P[s];t) == P[t] \mwedge{} (\mforall{}s:term(opr). (s << t {}\mRightarrow{} P[s]))
Date html generated:
2020_05_19-PM-09_54_32
Last ObjectModification:
2020_03_10-AM-11_21_31
Theory : terms
Home
Index