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