Nuprl Lemma : FOL-hyps-meaning-cons
∀[hyps,Dom,S,a,x:Top].
  (tuple-type(FOL-hyps-meaning(Dom;S;a;[x / hyps])) ~ if null(hyps)
  then Dom,S,a +|= FOL-abstract(x)
  else Dom,S,a +|= FOL-abstract(x) × tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
  fi )
Proof
Definitions occuring in Statement : 
FOL-hyps-meaning: FOL-hyps-meaning(Dom;S;a;hyps)
, 
FOL-abstract: FOL-abstract(fmla)
, 
FOSatWith+: Dom,S,a +|= fmla
, 
tuple-type: tuple-type(L)
, 
null: null(as)
, 
cons: [a / b]
, 
ifthenelse: if b then t else f fi 
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
product: x:A × B[x]
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
FOL-hyps-meaning: FOL-hyps-meaning(Dom;S;a;hyps)
, 
all: ∀x:A. B[x]
, 
top: Top
Lemmas referenced : 
map_cons_lemma, 
tupletype_cons_lemma, 
null-map, 
top_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
lemma_by_obid, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
isect_memberEquality, 
voidElimination, 
voidEquality, 
hypothesis, 
isectElimination, 
hypothesisEquality, 
sqequalAxiom, 
because_Cache
Latex:
\mforall{}[hyps,Dom,S,a,x:Top].
    (tuple-type(FOL-hyps-meaning(Dom;S;a;[x  /  hyps]))  \msim{}  if  null(hyps)
    then  Dom,S,a  +|=  FOL-abstract(x)
    else  Dom,S,a  +|=  FOL-abstract(x)  \mtimes{}  tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
    fi  )
Date html generated:
2016_05_15-PM-10_26_51
Last ObjectModification:
2015_12_27-PM-06_26_26
Theory : minimal-first-order-logic
Home
Index