Nuprl Definition : mFOL-sequent-freevars
mFOL-sequent-freevars(s) ==  let hs,c = s in reduce(λh,vs. mFOL-freevars(h) ⋃ vs;mFOL-freevars(c);hs)
Definitions occuring in Statement : 
mFOL-freevars: mFOL-freevars(fmla)
, 
l-union: as ⋃ bs
, 
reduce: reduce(f;k;as)
, 
int-deq: IntDeq
, 
lambda: λx.A[x]
, 
spread: spread def
Definitions occuring in definition : 
spread: spread def, 
reduce: reduce(f;k;as)
, 
lambda: λx.A[x]
, 
l-union: as ⋃ bs
, 
int-deq: IntDeq
, 
mFOL-freevars: mFOL-freevars(fmla)
FDL editor aliases : 
mFOL-sequent-freevars
Latex:
mFOL-sequent-freevars(s)  ==    let  hs,c  =  s  in  reduce(\mlambda{}h,vs.  mFOL-freevars(h)  \mcup{}  vs;mFOL-freevars(c);hs\000C)
Date html generated:
2016_05_15-PM-10_26_01
Last ObjectModification:
2015_09_23-AM-08_25_23
Theory : minimal-first-order-logic
Home
Index