Nuprl Lemma : mFOL-sequent-evidence_and
From uniform evidence that hyps 
⇒ x and 
uniform evidence that (y ∧ hyps) 
⇒ y
we construct uniform evidence that hyps 
⇒ x ∧ y⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-sequent-evidence(<hyps, x>) 
⇒ mFOL-sequent-evidence(<hyps, y>) 
⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ y>))
Proof
Definitions occuring in Statement : 
mFOL-sequent-evidence: mFOL-sequent-evidence(s)
, 
mFOconnect: mFOconnect(knd;left;right)
, 
mFOL: mFOL()
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
pair: <a, b>
, 
token: "$token"
Lemmas : 
tuple-type_wf, 
map_wf, 
mFOL_wf, 
FOSatWith_wf, 
mFOL-abstract_wf, 
FOAssignment_wf, 
FOStruct_wf, 
mFOL-sequent-evidence_wf, 
list_wf
\mforall{}hyps:mFOL()  List.  \mforall{}[x,y:mFOL()].    (mFOL-sequent-evidence(<hyps,  x>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,\000C  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x  \mwedge{}  y>))
Date html generated:
2015_07_17-AM-07_56_41
Last ObjectModification:
2015_01_27-AM-10_05_24
Home
Index