Nuprl Lemma : sys-subformulas_wf
∀[S:Top]. (sys-subformulas(S) ∈ Type)
Proof
Definitions occuring in Statement :
sys-subformulas: sys-subformulas(S),
uall: ∀[x:A]. B[x],
top: Top,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
sys-subformulas: sys-subformulas(S),
prop: ℙ
Lemmas referenced :
dl-prop_wf,
true_wf,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
setEquality,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[S:Top]. (sys-subformulas(S) \mmember{} Type)
Date html generated:
2019_10_16-AM-11_24_57
Last ObjectModification:
2019_05_04-PM-06_27_39
Theory : dynamic!logic
Home
Index