Nuprl Definition : list-strict
list-strict(F) ==
(∀x:Base
((F 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 <x, y> ~ G (F y) x y)) ∧ strict(G)))
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],
and: P ∧ Q,
all: ∀x:A. B[x],
base: Base,
sqequal: s ~ t,
pair: <a, b>,
apply: f a,
strict: strict(F)
FDL editor aliases :
list-strict
Latex:
list-strict(F) ==
(\mforall{}x:Base
((F 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 <x, y> \msim{} G (F y) x y)) \mwedge{} strict(G)))
Date html generated:
2016_05_15-PM-10_07_46
Last ObjectModification:
2015_09_23-AM-08_22_20
Theory : eval!all
Home
Index