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