Nuprl Definition : l-strict
l-strict(F) ==
∀r:Base
((∀x:Base
((F r x)↓
⇒ ((∀a,b:Base. (if x is a pair then a otherwise b ~ a)) ∨ (∀a,b:Base. (if x = Ax then a otherwise b ~ a)))))
∧ (∃G:Base. ∀x,y:Base. ((F r <x, y> ~ G x y (r y)) ∧ strict(G x y))))
Definitions occuring in Statement :
strict: strict(F),
has-value: (a)↓,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
pair: <a, b>,
base: Base,
sqequal: s ~ t
Definitions occuring in definition :
implies: P ⇒ Q,
has-value: (a)↓,
or: P ∨ Q,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
base: Base,
and: P ∧ Q,
sqequal: s ~ t,
pair: <a, b>,
strict: strict(F),
apply: f a
FDL editor aliases :
l-strict
Latex:
l-strict(F) ==
\mforall{}r:Base
((\mforall{}x:Base
((F r x)\mdownarrow{}
{}\mRightarrow{} ((\mforall{}a,b:Base. (if x is a pair then a otherwise b \msim{} a))
\mvee{} (\mforall{}a,b:Base. (if x = Ax then a otherwise b \msim{} a)))))
\mwedge{} (\mexists{}G:Base. \mforall{}x,y:Base. ((F r <x, y> \msim{} G x y (r y)) \mwedge{} strict(G x y))))
Date html generated:
2016_05_13-PM-03_23_56
Last ObjectModification:
2015_09_22-PM-05_44_43
Theory : call!by!value_1
Home
Index