Nuprl Definition : p-mu
p-mu(P;x) == case x of inl(n) => (↑(P n)) ∧ (∀i:ℕn. (¬↑(P i))) | inr(z) => ∀i:ℕ. (¬↑(P i))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
and: P ∧ Q,
int_seg: {i..j-},
natural_number: $n,
all: ∀x:A. B[x],
nat: ℕ,
not: ¬A,
assert: ↑b,
apply: f a
FDL editor aliases :
p-mu
Latex:
p-mu(P;x) == case x of inl(n) => (\muparrow{}(P n)) \mwedge{} (\mforall{}i:\mBbbN{}n. (\mneg{}\muparrow{}(P i))) | inr(z) => \mforall{}i:\mBbbN{}. (\mneg{}\muparrow{}(P i))
Date html generated:
2016_05_15-PM-03_32_39
Last ObjectModification:
2015_09_23-AM-07_44_04
Theory : general
Home
Index