Nuprl Lemma : dl_forces_wf
∀[K:dl_KS]. ∀[a:Prop]. ∀[s:worlds(K)]. ∀[pos:𝔹]. (dl_forces(K;pos;a;s) ∈ ℙ)
Proof
Definitions occuring in Statement :
dl_forces: dl_forces(K;pos;a;s),
dl_KS: dl_KS,
worlds: worlds(k),
dl-prop: Prop,
bool: 𝔹,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
prop: ℙ,
subtype_rel: A ⊆r B,
dl_forces: dl_forces(K;pos;a;s),
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
and: P ∧ Q,
so_apply: x[s],
so_lambda: so_lambda4,
exists: ∃x:A. B[x],
so_apply: x[s1;s2;s3;s4],
or: P ∨ Q,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
dl-kind: dl-kind(d),
mobj-kind: mobj-kind(x),
pi1: fst(t),
dl-prop-obj: prop(x),
bfalse: ff
Lemmas referenced :
dl_KS_wf,
dl-prop_wf,
dl_KS_subtype,
bool_wf,
subtype-TYPE,
worlds_wf,
dl-ind_wf_definition,
KrRel_wf,
atmFrc_prog_wf,
istype-nat,
subtype_rel_self,
dl-prog_wf,
rel_star_wf,
btrue_wf,
equal_wf,
atmFrc_prop_wf,
ifthenelse_wf,
false_wf,
true_wf,
bfalse_wf,
dl-prop-obj_wf
Rules used in proof :
universeIsType,
instantiate,
universeEquality,
sqequalRule,
hypothesis,
because_Cache,
applyEquality,
hypothesisEquality,
cumulativity,
functionEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
lambdaEquality_alt,
productEquality,
inhabitedIsType,
functionIsType,
unionEquality,
dependent_functionElimination
Latex:
\mforall{}[K:dl\_KS]. \mforall{}[a:Prop]. \mforall{}[s:worlds(K)]. \mforall{}[pos:\mBbbB{}]. (dl\_forces(K;pos;a;s) \mmember{} \mBbbP{})
Date html generated:
2020_05_20-AM-09_01_48
Last ObjectModification:
2020_01_17-PM-02_25_04
Theory : dynamic!logic
Home
Index