Nuprl Definition : node_complete
node_complete{i:l}(n) ==
(∀f∈fst(n).(∀f1∈localT prop(f).(f1 ∈ fst(n)))) ∧ (∀f∈snd(n).(∀f1∈localF prop(f).(f1 ∈ snd(n))))
Definitions occuring in Statement :
dl-localF: localF,
dl-localT: localT,
dl-prop-obj: prop(x),
dl-prop: Prop,
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
apply: f a
Definitions occuring in definition :
and: P ∧ Q,
dl-localT: localT,
pi1: fst(t),
l_all: (∀x∈L.P[x]),
apply: f a,
dl-localF: localF,
dl-prop-obj: prop(x),
l_member: (x ∈ l),
pi2: snd(t),
dl-prop: Prop
FDL editor aliases :
node_complete
Latex:
node\_complete\{i:l\}(n) ==
(\mforall{}f\mmember{}fst(n).(\mforall{}f1\mmember{}localT prop(f).(f1 \mmember{} fst(n)))) \mwedge{} (\mforall{}f\mmember{}snd(n).(\mforall{}f1\mmember{}localF prop(f).(f1 \mmember{} snd(n))))
Date html generated:
2020_05_20-AM-09_02_02
Last ObjectModification:
2019_11_27-PM-02_28_59
Theory : dynamic!logic
Home
Index