Nuprl Lemma : dl-kind_wf
∀[d:dl-Obj()]. (dl-kind(d) ∈ {a:Atom| (a ∈ ``prog prop``)} )
Proof
Definitions occuring in Statement :
dl-kind: dl-kind(d),
dl-Obj: dl-Obj(),
l_member: (x ∈ l),
cons: [a / b],
nil: [],
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
token: "$token",
atom: Atom
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
mkinds: mKinds,
cons: [a / b],
eager-map: eager-map(f;as),
list_ind: list_ind,
dl-Spec: dl-Spec(),
pi1: fst(t),
nil: [],
it: ⋅,
dl-Obj: dl-Obj(),
dl-kind: dl-kind(d)
Lemmas referenced :
mobj-kind_wf,
dl-Spec_wf,
dl-Obj_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
extract_by_obid,
isectElimination,
thin,
hypothesis,
hypothesisEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
universeIsType
Latex:
\mforall{}[d:dl-Obj()]. (dl-kind(d) \mmember{} \{a:Atom| (a \mmember{} ``prog prop``)\} )
Date html generated:
2019_10_15-AM-11_39_58
Last ObjectModification:
2019_03_26-AM-11_24_26
Theory : dynamic!logic
Home
Index