Nuprl Lemma : FOSatWith_wf
∀[Dom:Type]. ∀[S:FOStruct(Dom)]. ∀[a:FOAssignment(Dom)]. ∀[fmla:AbstractFOFormula]. (Dom,S,a |= fmla ∈ ℙ)
Proof
Definitions occuring in Statement :
FOSatWith: Dom,S,a |= fmla,
AbstractFOFormula: AbstractFOFormula,
FOStruct: FOStruct(Dom),
FOAssignment: FOAssignment(Dom),
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
universe: Type
Lemmas :
AbstractFOFormula_wf,
FOAssignment_wf,
FOStruct_wf
\mforall{}[Dom:Type]. \mforall{}[S:FOStruct(Dom)]. \mforall{}[a:FOAssignment(Dom)]. \mforall{}[fmla:AbstractFOFormula].
(Dom,S,a |= fmla \mmember{} \mBbbP{})
Date html generated:
2015_07_17-AM-07_53_12
Last ObjectModification:
2015_01_27-AM-10_07_18
Home
Index