Nuprl Definition : mFOL-sequent-abstract
The abstract meaning of a sequent is a function
from the tuple of abstract meanings of the hypotheses to
the abstract meaning of the conclusion.⋅
mFOL-sequent-abstract(s) ==
  let hyps,concl = s 
  in λDom,S,a. (tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps)) ─→ Dom,S,a |= mFOL-abstract(concl))
Definitions occuring in Statement : 
mFOL-abstract: mFOL-abstract(fmla)
, 
FOSatWith: Dom,S,a |= fmla
, 
tuple-type: tuple-type(L)
, 
map: map(f;as)
, 
lambda: λx.A[x]
, 
function: x:A ─→ B[x]
, 
spread: spread def
FDL editor aliases : 
mFOL-sequent-abstract
mFOL-sequent-abstract(s)  ==
    let  hyps,concl  =  s 
    in  \mlambda{}Dom,S,a.  (tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);hyps))
                            {}\mrightarrow{}  Dom,S,a  |=  mFOL-abstract(concl))
Date html generated:
2015_07_17-AM-07_56_29
Last ObjectModification:
2012_09_11-PM-05_45_32
Home
Index