Nuprl Lemma : mFOL-sequent-evidence_and

From uniform evidence that hyps  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>))


Definitions occuring in Statement :  mFOL-sequent-evidence: mFOL-sequent-evidence(s) mFOconnect: mFOconnect(knd;left;right) mFOL: mFOL() list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  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