Nuprl Definition : p-graph
p-graph(A;f) == λx,y. ((↑can-apply(f;x)) c∧ (y = do-apply(f;x) ∈ A))
Definitions occuring in Statement :
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
assert: ↑b,
cand: A c∧ B,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
cand: A c∧ B,
assert: ↑b,
can-apply: can-apply(f;x),
equal: s = t ∈ T,
do-apply: do-apply(f;x)
FDL editor aliases :
p-graph
Latex:
p-graph(A;f) == \mlambda{}x,y. ((\muparrow{}can-apply(f;x)) c\mwedge{} (y = do-apply(f;x)))
Date html generated:
2016_05_15-PM-04_34_15
Last ObjectModification:
2015_09_23-AM-07_49_15
Theory : general
Home
Index