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