Nuprl Lemma : Rref_wf
∀[K:dl_KS]. ∀i:worlds(K). (Rref(K;i) ∈ iRi)
Proof
Definitions occuring in Statement :
Rref: Rref(k;i),
dl_KS: dl_KS,
KrRel: sRt,
worlds: worlds(k),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
Rref: Rref(k;i),
dl_KS: dl_KS,
record+: record+,
record-select: r.x,
subtype_rel: A ⊆r B,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
btrue: tt,
prop: ℙ,
implies: P ⇒ Q
Lemmas referenced :
subtype_rel_self,
worlds_wf,
KrRel_wf,
nat_wf,
atmFrc_prop_wf,
dl_KS_subtype,
dl_KS_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
lambdaFormation_alt,
sqequalRule,
sqequalHypSubstitution,
dependentIntersectionElimination,
dependentIntersectionEqElimination,
thin,
hypothesis,
applyEquality,
tokenEquality,
extract_by_obid,
isectElimination,
functionEquality,
hypothesisEquality,
functionExtensionality,
universeIsType,
lambdaEquality_alt,
dependent_functionElimination,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionIsTypeImplies,
inhabitedIsType
Latex:
\mforall{}[K:dl\_KS]. \mforall{}i:worlds(K). (Rref(K;i) \mmember{} iRi)
Date html generated:
2020_05_20-AM-09_01_33
Last ObjectModification:
2019_11_27-PM-02_24_54
Theory : dynamic!logic
Home
Index