Nuprl Definition : AF-spread-law
AF-spread-law(x,y.R[x; y]) == λn,s,x. ((↑isl(x)) ⇒ (∀i:ℕn. ((↑isl(s i)) ∧ (¬R[outl(s i); outl(x)]))))
Definitions occuring in Statement :
int_seg: {i..j-},
outl: outl(x),
assert: ↑b,
isl: isl(x),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
and: P ∧ Q,
assert: ↑b,
isl: isl(x),
not: ¬A,
apply: f a,
outl: outl(x)
FDL editor aliases :
AF-spread-law
Latex:
AF-spread-law(x,y.R[x; y]) ==
\mlambda{}n,s,x. ((\muparrow{}isl(x)) {}\mRightarrow{} (\mforall{}i:\mBbbN{}n. ((\muparrow{}isl(s i)) \mwedge{} (\mneg{}R[outl(s i); outl(x)]))))
Date html generated:
2016_05_13-PM-03_50_55
Last ObjectModification:
2015_09_22-PM-05_45_22
Theory : bar-induction
Home
Index