Nuprl Definition : binders-disjoint
binders-disjoint(opr;L;t) ==
case t
of inl(v) =>
True
| inr(p) =>
let op,bts = p
in (∀bt∈bts.l_disjoint(varname();fst(bt);L) ∧ binders-disjoint(opr;L;snd(bt)))
Definitions occuring in Statement :
varname: varname(),
l_disjoint: l_disjoint(T;l1;l2),
l_all: (∀x∈L.P[x]),
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
true: True,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
true: True,
spread: spread def,
l_all: (∀x∈L.P[x]),
and: P ∧ Q,
l_disjoint: l_disjoint(T;l1;l2),
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
binders-disjoint
Latex:
binders-disjoint(opr;L;t) ==
case t
of inl(v) =>
True
| inr(p) =>
let op,bts = p
in (\mforall{}bt\mmember{}bts.l\_disjoint(varname();fst(bt);L) \mwedge{} binders-disjoint(opr;L;snd(bt)))
Date html generated:
2020_05_19-PM-09_56_19
Last ObjectModification:
2020_03_09-PM-04_09_19
Theory : terms
Home
Index