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